一个高级结构同一性原理
A Higher Structure Identity Principle
摘要：
普通的结构同一性原则指出集合水平结构的任何性质（例如，偏序集，群，环，域）在同构下是不变的：更具体地说，结构的标识与同构一致。我们证明了这一原则的一个版本，广泛的高类别的结构，适应FOLDS签名，以指定一个一般的结构类，并使用两级类型理论对待所有类别的尺寸一致。正如先前已知的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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
