University of Birmingham > Talks@bham > Theoretical computer science seminar >  Identity, indiscernibility, and univalence: a higher structure identity principle

Identity, indiscernibility, and univalence: a higher structure identity principle

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

If you have a question about this talk, please contact Paul Levy.

https://us04web.zoom.us/j/2517319462

The Structure Identity Principle in univalent type theory says that for a range of structures in ordinary mathematics, identity is equivalent to isomorphism, with the consequence that isomorphic structures are formally indiscernible. A similar principle says that for categories, identity is equivalent to equivalence, so that equivalent categories are also indiscernible, as long as the categories themselves satisfy a SIP for their objects. We generalize these principles to a wide range of categorical and higher-categorical structures, using a notion of signature for higher structures inspired by Makkai’s First-Order Logic with Dependent Sorts; the general SIP for objects requires structures to satisfy a relativized form of the identity of indiscernibles. This is joint work with Benedikt Ahrens, Paige North, and Dimitris Tsementzis.

This talk is part of the Theoretical computer science seminar series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on talks.cam from the University of Cambridge.