一句话：在 HoTT 中用高阶归纳类型表示整数，避免集合截断并验证其与带符号自然数表示等价。
在 Homotopy Type Theory 中定义整数时，带符号自然数（余积）的归纳原理会导致大量情况分支，而集合商需要 set-truncation，所得递归原理只能定义到集合的函数。本文提出用高阶归纳类型表示整数，分别基于小宇宙（small universe）与 bi-invertible maps 两种构造，从而无需显式 set-truncation。作者证明这些类型与通常的余积表示等价，并说明该例子如何体现 HoTT 中 coherence 问题的处理。所有证明已在 cubical 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.