Abstract

https://us02web.zoom.us/j/177472153?pwd=MFgwd0EzY05QSGtpSDc2dU16aG9wdz09

There is a nominal approach to higher dimensional structure using sets whose elements are supported by finite subsets of an “unfinite” set of named dimensions (x-axis, y-axis, z-axis, etc.), modulo permutation symmetry of the named dimensions. For example, an element whose support is {x,y,z} has dimenion 3. By considering such sets equipped with a simple notion of end-point (0/1) substitution, one arrives at a category equivalent to the category of cubical sets (with name abstraction corresponding to path objects) that is the starting point for the Bezem-Coquand-Huber model of homotopy type theory (HoTT). (See Pitts, Proc. TYPES 2014 .)

I will sketch these ideas and then show how strict cubical omega-categories can be defined quite simply in this style (using the formulation of “category” in which objects are identified with identity morphisms). I will also speculate why this might be interesting from the point of view of models of HoTT.