TY - UNPB

T1 - A Higher Structure Identity Principle

AU - Ahrens, Benedikt

AU - North, Paige Randall

AU - Shulman, Michael

AU - Tsementzis, Dimitris

N1 - Long version of publication in LICS 2020 (DOI: 10.1145/3373718.3394755); v2: added sections "Axioms and Theories" and "Version History", other minor changes; v3: added examples

PY - 2020/4/14

Y1 - 2020/4/14

N2 - 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.

AB - 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.

KW - math.LO

KW - cs.LO

KW - math.CT

U2 - 10.48550/arXiv.2004.06572

DO - 10.48550/arXiv.2004.06572

M3 - Preprint

SP - 1

EP - 41

BT - A Higher Structure Identity Principle

PB - arXiv

ER -