一句话：将结构同一性原理推广到广泛的高阶范畴结构，并用双层次类型论与 FOLDS 签名刻画不可区分性。
普通结构同一性原理断言：集合层面的结构（如偏序集、群、环、域）在 Univalent Foundations 中可定义的性质在同构下不变，且结构的同一等同于同构。本文把该原理推广到一大类高阶范畴结构。作者将 FOLDS 签名改造为指定这类结构的一般框架，并采用双层次类型论（two-level type theory）统一处理各范畴维度。与已知的 1-范畴情形一样，结构本身须满足局部 univalence 原理，即元素间的同一等同于元素间的“同构”。主要技术贡献是定义这种同构——称为 indiscernibility——且该定义只依赖依赖结构，而不使用任何复合概念。
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.