n-截断类型论中的部分单叶性
Partial Univalence in n-truncated Type Theory
摘要：
众所周知，univalence与unique of identity proofs（UIP）是不相容的，UIP是所有类型都是h-集的公理。这是由于有限的h-集只要不是h-命题就有非平凡的自同构。一个自然的问题是，限制于h-命题的单价是否与UIP相容。我们通过构建一个模型来肯定地回答这个问题，在这个模型中，类型是同伦类型论中定义为更高归纳类型的封闭宇宙的元素。这个宇宙有一个同时“部分”单价完成的路径构造器，即，仅限于H命题。更一般地说，我们表明，单价限于$(n-1)$类型是一致的假设，所有类型的$n$截断。此外，我们参数化我们的建设一个适当的良好的行为容器，抽象从一个具体的选择类型的former的宇宙。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
