从高阶截断中构造函数

在同伦类型论中，当不关心类型的高阶结构并希望避免余环问题时，截断算子 ||-||n（对于数字 n > -2）通常非常有用。然而，其消去原理仅允许消去到 n-类型中，这使得当 B 不是 n-类型时，很难构造函数 ||A||n -> B。这使得推导更强大的消去定理变得很有必要。我们展示了一个初步的一般性结果：如果 B 是一个 (n+1)-类型，那么函数 ||A||n -> B 精确对应于在所有 (n+1) �阶环路空间上为常值的函数 A -> B。我们给出了一个“初等”证明和一个使用高阶归纳类型的证明，两者都需要付出一些努力。作为我们结果的一个示例应用，我们展示了只要 1-类型具有“辫状”环路空间，我们就可以构造其“基于集合”的表示。主要结果及其证明之一以及该应用已在 Agda 中形式化。