单价原则
The Univalence Principle
摘要：
单价原理是这样一种陈述，等价的数学结构是不可区分的。我们证明了这一原理的一般版本，适用于以非代数和基于空间的风格定义的所有基于集合的、范畴的和更高范畴的结构，以及高阶理论（例如拓扑空间）的模型。特别是，我们制定了一个一般的定义，任何这样的结构的对象的不可分割性，和相应的单性条件，推广Rezk的完整性条件的Segal空间，并确保所有等价的结构是levelwise等价。我们的工作建立在Makkai的一阶逻辑与相关排序，但表示在Voevodsky的单价基础（UF），扩展以前的工作的结构同一性原则和单价类别UF。这使得不可否认性可以简单地表示为识别，并产生一个正式的理论，在经典同伦理论中是可解释的，但也在其他更高的拓扑模型。由此可见，单价基础是更高范畴数学的完全等价不变基础，正如Voevodsky所意图的那样。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
