A Higher Structure Identity Principle

Benedikt Ahrens, Paige Randall North, Michael Shulman, Dimitris Tsementzis

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.
Original languageEnglish
Title of host publication35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2020)
PublisherIEEE Computer Society Press
Number of pages14
Publication statusAccepted/In press - 11 Apr 2020
Event35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2020) - Online
Duration: 8 Jul 202011 Jul 2020


Conference35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2020)


  • homotopy type theory
  • univalent foundations
  • structure identity principle
  • categories
  • equivalence principle


Dive into the research topics of 'A Higher Structure Identity Principle'. Together they form a unique fingerprint.

Cite this