论文标题
整数作为较高的电感类型
The Integers as a Higher Inductive Type
论文作者
论文摘要
我们考虑定义整数在同型类型理论（HOTT）中的问题。我们可以将整数的类型定义为签名的自然数（即使用相关数），但是它的诱导原理很不便，因为它会导致病例爆炸。一种替代方法是使用设定的品质，但是在这里我们需要使用设定截断来避免非平凡的较高平等性。这导致递归原理，该原理只允许我们将函数定义为集合（满足UIP的类型）。在本文中，我们考虑使用小型宇宙或双可变图考虑更高的感应类型。这些类型代表整数没有明确的设置截断，等效于通常的共同体表示。这是一个有趣的例子，因为它显示了如何在Hott中处理一些连贯性问题。我们讨论了这项工作引起的一些开放问题。使用立方AGDA对证明进行了正式验证。
We consider the problem of defining the integers in Homotopy Type Theory (HoTT). We can define the type of integers as signed natural numbers (i.e., using a coproduct), but its induction principle is very inconvenient to work with, since it leads to an explosion of cases. An alternative is to use set-quotients, but here we need to use set-truncation to avoid non-trivial higher equalities. This results in a recursion principle that only allows us to define function into sets (types satisfying UIP). In this paper we consider higher inductive types using either a small universe or bi-invertible maps. These types represent integers without explicit set-truncation that are equivalent to the usual coproduct representation. This is an interesting example since it shows how some coherence problems can be handled in HoTT. We discuss some open questions triggered by this work. The proofs have been formally verified using cubical Agda.
