Abstract
The ordinary Structure Identity Principle states that any property of set-level structures (e.g., posets, groups, rings, fields) definable in Univalent Foundations is invariant under isomorphism: more specifically, identifications of structures coincide with isomorphisms. We prove a version of this
principle for a wide range of higher-categorical structures, adapting FOLDS-signatures to specify a general class of structures, and using two-level type theory to treat all categorical dimensions uniformly. As in the previously known case of 1-categories (which is an instance of our theory), the structures themselves must satisfy a local univalence principle, stating that identifications coincide with “isomorphisms” between elements of the structure. Our main technical achievement is a definition of such isomorphisms, which we call “indiscernibilities,” using only the dependency structure rather than any notion of composition.
principle for a wide range of higher-categorical structures, adapting FOLDS-signatures to specify a general class of structures, and using two-level type theory to treat all categorical dimensions uniformly. As in the previously known case of 1-categories (which is an instance of our theory), the structures themselves must satisfy a local univalence principle, stating that identifications coincide with “isomorphisms” between elements of the structure. Our main technical achievement is a definition of such isomorphisms, which we call “indiscernibilities,” using only the dependency structure rather than any notion of composition.
Original language | English |
---|---|
Title of host publication | 35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2020) |
Publisher | IEEE Computer Society Press |
Number of pages | 14 |
Publication status | Accepted/In press - 11 Apr 2020 |
Event | 35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2020) - Online Duration: 8 Jul 2020 → 11 Jul 2020 |
Conference
Conference | 35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2020) |
---|---|
City | Online |
Period | 8/07/20 → 11/07/20 |
Keywords
- homotopy type theory
- univalent foundations
- structure identity principle
- categories
- equivalence principle