University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > Unfinity Categories

Unfinity Categories

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Jamie Vicary.

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.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2021 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity