The Integers as a Higher Inductive Type
The Integers as a Higher Inductive Type
复制标题
整数作为更高归纳类型
DOI：
10.1145/3373718.3394760
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
Altenkirch T
中科院分区：
文献类型：
--
作者：
Altenkirch T
我们考虑同伦型理论(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.
登录
查看更多内容
影响因子：
1.8
作者：
Vezzosi, Andrea;Mortberg, Anders;Abel, Andreas
通讯作者：
Abel, Andreas
同伦型理论中的自由高级群
DOI：
10.1145/3209108.3209183
发表时间：
2018
期刊：
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science
影响因子：
--
作者：
Nicolai Kraus;Thorsten Altenkirch
通讯作者：
Thorsten Altenkirch
更高电感-电感类型的签名和感应原理
DOI：
10.23638/lmcs-16(1:10)2020
发表时间：
2019
期刊：
Log. Methods Comput. Sci.
影响因子：
--
作者：
A. Kaposi;A. Kovács
通讯作者：
A. Kovács
立方类型理论中的更高归纳类型
DOI：
10.1145/3209108.3209197
发表时间：
2018
期刊：
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science
影响因子：
--
作者：
T. Coquand;Simon Huber;Anders Mörtberg
通讯作者：
Anders Mörtberg
同伦型理论
DOI：
10.1007/978-3-662-45824-2_1
发表时间：
2015
期刊：
Higher Categories and Homotopical Algebra
影响因子：
--
作者：
S. Awodey
通讯作者：
S. Awodey