Unfinity Categories

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

• Andrew Pitts, University of Cambridge
• Friday 26 March 2021, 14:00-15:00
• Online.

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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• Online
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.