08/07/2020

A Higher Structure Identity Principle

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

Keywords: equivalence principle, structure identity principle, categories, homotopy type theory, univalent foundations

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.

 0
 0
 0
 0
This is an embedded video. Talk and the respective paper are published at ICALP 2020 virtual conference. If you are one of the authors of the paper and want to manage your upload, see the question "My papertalk has been externally embedded..." in the FAQ section.

Comments

Post Comment
no comments yet
code of conduct: tbd

Similar Papers