论文标题
较高的结构身份原理
A Higher Structure Identity Principle
论文作者
论文摘要
普通的结构认同原则指出，在单相基础中可以定义的设定级结构（例如POSET，组，环，田地）的任何特性在同构基础下都是不变的：更具体地说，结构的识别与同构相吻合。我们证明了该原理的一个版本，用于广泛的更高分类结构，适应折叠式签名来指定一般的结构类别，并使用两级类型的理论均匀地对待所有分类维度。就像在先前已知的1类情况下（这是我们理论的一个实例）一样，结构本身必须满足局部单位原则，并指出识别与结构元素之间的“同构”一致。我们的主要技术成就是对此类同构的定义，我们称之为“不明智”，仅使用依赖性结构而不是任何组成概念。
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.
