论文标题
n截断类型理论的部分无关
Partial Univalence in n-truncated Type Theory
论文作者
论文摘要
众所周知，单位与身份证明的独特性（UIP）不相容，这是所有类型都是H-set的公理。这是由于有限的H-set具有非平凡的自动形态，一旦它们不是H构态。 一个自然的问题是，仅限于h-构的单位性是否与UIP兼容。我们通过构建模型是封闭的宇宙的元素来回答这一问题，该模型被定义为同型类型理论中较高的电感类型。这个宇宙具有同时“部分”单价完成的路径构造变量，即仅限于H个性。 更普遍的是，我们表明，仅限$（n-1）$ - 类型的单相限制与所有类型均为$ n $截断的假设是一致的。此外，我们通过一个适当举止良好的容器来对构造进行参数，以从宇宙的类型构造器选择中抽象。
It is well known that univalence is incompatible with uniqueness of identity proofs (UIP), the axiom that all types are h-sets. This is due to finite h-sets having non-trivial automorphisms as soon as they are not h-propositions. A natural question is then whether univalence restricted to h-propositions is compatible with UIP. We answer this affirmatively by constructing a model where types are elements of a closed universe defined as a higher inductive type in homotopy type theory. This universe has a path constructor for simultaneous "partial" univalent completion, i.e., restricted to h-propositions. More generally, we show that univalence restricted to $(n-1)$-types is consistent with the assumption that all types are $n$-truncated. Moreover we parametrize our construction by a suitably well-behaved container, to abstract from a concrete choice of type formers for the universe.
