Higher inductive types (HITs) in homotopy type theory are a powerful generalization of inductive types. Not only can they have ordinary constructors to define elements, but also higher constructors to define equalities (paths). We say that a HIT H is non-recursive if its constructors do not quantify over elements or paths in H. The advantage of non-recursive HITs is that their elimination principles are easier to apply than those of general HITs. udIt is an open question which classes of HITs can be encoded as non-recursive HITs. One result of this paper is the construction of the propositional truncation via a sequence of approximations, yielding a representation as a non-recursive HIT. Compared to a related construction by van Doorn, ours has the advantage that the connectedness level increases in each step, yielding simplified elimination principles into n-types. As the elimination principle of our sequence has strictly lower requirements, we can then prove a similar result for van Doorn’s construction. We further derive general elimination principles of higher truncations (say, k-truncations) into n-types, generalizing a previous result by Capriotti et al. which considered the case n=k+1.
展开▼
机译：同伦类型理论中的高级归纳类型（HIT）是归纳类型的有力概括。他们不仅可以使用普通的构造函数来定义元素，而且还可以使用高级构造函数来定义等式（路径）。我们说，如果HIT H的构造函数未对H中的元素或路径进行量化，则它是非递归的。非递归HIT的优点在于，它们的消除原理比普通HIT的消除原理更容易应用。 ud这是一个开放性问题，哪些HIT类别可以编码为非递归HIT。本文的一个结果是通过一系列逼近来构造命题截断，从而表示为非递归HIT。与范·多恩（van Doorn）的相关构造相比，我们的优势在于，连接程度在每个步骤中都会增加，从而将简化的消除原理转化为n型。由于我们序列的消除原理严格要求较低，因此我们可以证明范·多恩的构造具有类似的结果。我们进一步推导了将高位截断（例如k截断）转换为n型的一般消除原理，从而概括了Capriotti等人的先前结果。考虑了n = k + 1的情况。
展开▼
