统一原则 (The Univalence Principle)

from arxiv, A short version of this book is available as arXiv:2004.06572. v2: added references and some details on morphisms of premonoidal categories

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.

翻译：统一原则是相当的数学结构是不可分的。我们证明了这一原则的通用版本,它适用于所有基于固定的、绝对的和基于空间的形态定义的所有定型、绝对的和较高的分类结构,以及高阶理论模型,如地形空间。特别是,我们对任何此类结构的物体的不易分化性制定了一般定义,以及相应的单一条件,该条件概括了雷兹克对安全空间的完整性条件,并确保结构的所有等同都是等同水平的。我们的工作以马克开之以离子排序的第一正态逻辑为基础,但表现在Voevofodsky的Univalent基金会(UF)中,扩展了以前关于结构特性原则和UFUF中单向类别的工作。这可以将不可分性仅仅表现为识别,并产生一种正式的理论,可以在古典同质理论中加以解释,但在其他更高的模型中也可加以解释。由此推论, 大学基础是一个完全等值的数学基础,通过高等值的数学基础。