Towards a Higher Structure Identity Principle

The Structure Identity Principle (SIP) is an informal principle asserting that isomorphic structures are equal. In univalent foundations, the SIP can be formally stated and proved for a variety of mathematical structures. This means that any statement that can be expressed in univalent foundations is invariant under isomorphism, or, put differently, that only structural properties can be stated in univalent foundations.

The SIP only applies to objects that naturally form a 1-category. In
this talk, we discuss work in progress towards a Higher Structure
Identity Principle in univalent foundations, for structures that naturally form a higher category (e.g., categories themselves).

I will strive to make the talk self-contained by starting with an overview of type theory and univalent foundations.

This is joint work with Paige North, Mike Shulman, and Dimitris Tsementzis,