A Higher Structure Identity Principle

DOI10.1145/3373718.3394755zbMath1498.03027arXiv2004.06572OpenAlexW3101135346MaRDI QIDQ5145618

Benedikt Ahrens, Michael Shulman, Paige Randall North, 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 theoryunivalent foundationsstructure identity principle

Mathematics Subject Classification ID

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

Related Items

Bicategories in univalent foundations ⋮ Two-level type theory and applications