A higher structure identity principle

DOI10.1145/3373718.3394755MaRDI QIDQ5145618zbMATH OpenOpenAlexFDO

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

Publication date 21 January 2021

Published in Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2004.06572

zbMATH Keywords

categoriesequivalence principlehomotopy type theorystructure identity principleunivalent foundations

Mathematics Subject Classification ID

Type theory (03B38) Metamathematics of constructive systems (03F50) Categories of fibrations, relations to (K)-theory, relations to type theory (18N45) Abstract and axiomatic homotopy theory in algebraic topology (55U35) Specification and verification (program logics, model checking, etc.) (68Q60)

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.

Recommendations

• Structuralism, Invariance, and Univalence
• Isomorphism is equality
• Univalence as a principle of logic
• The simplicial model of univalent foundations (after Voevodsky)
• Univalent foundations as structuralist foundations

Cited in

(7)

• Relativizations of the Principle of Identity
• Bicategories in univalent foundations
• Two-level type theory and applications
• Pregeometric spaces from Wolfram model rewriting systems as homotopy types
• Topological quantum gates in homotopy type theory
• On planarity of graphs in homotopy type theory
• Isomorphism is equality

This page was built for publication: A higher structure identity principle

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5145618)