
arXiv: 2102.06275
The Univalence Principle is the statement that equivalent mathematical structures are indistinguishable. We prove a general version of this principle that applies to all set-based, categorical, and higher-categorical structures defined in a non-algebraic and space-based style, as well as models of higher-order theories such as topological spaces. In particular, we formulate a general definition of indiscernibility for objects of any such structure, and a corresponding univalence condition that generalizes Rezk’s completeness condition for Segal spaces and ensures that all equivalences of structures are levelwise equivalences. Our work builds on Makkai’s First-Order Logic with Dependent Sorts, but is expressed in Voevodsky’s Univalent Foundations (UF), extending previous work on the Structure Identity Principle and univalent categories in UF. This enables indistinguishability to be expressed simply as identification, and yields a formal theory that is interpretable in classical homotopy theory, but also in other higher topos models. It follows that Univalent Foundations is a fully equivalence-invariant foundation for higher-categorical mathematics, as intended by Voevodsky.
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, 18N99, Mathematics - Category Theory, 18N99, 03B38, 03G30, 55U35, Mathematics - Logic, cs.LO, Logic in Computer Science (cs.LO), 03B38, math.LO, 03G30, FOS: Mathematics, Category Theory (math.CT), math.CT, 55U35, Logic (math.LO)
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, 18N99, Mathematics - Category Theory, 18N99, 03B38, 03G30, 55U35, Mathematics - Logic, cs.LO, Logic in Computer Science (cs.LO), 03B38, math.LO, 03G30, FOS: Mathematics, Category Theory (math.CT), math.CT, 55U35, Logic (math.LO)
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 2 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Top 10% | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
