## 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