The Integers as a Higher Inductive Type

Altenkirch, Thorsten; Scoccola, Luis

Abstract

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.

Citation

Altenkirch, T., & Scoccola, L. (2020, July). The Integers as a Higher Inductive Type. Presented at LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken Germany

• Presentation Conference Type: Edited Proceedings
• Conference Name: LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science
• Start Date: Jul 8, 2020
• End Date: Jul 11, 2020
• Acceptance Date: Apr 10, 2020
• Online Publication Date: Jul 6, 2020
• Publication Date: Jul 8, 2020
• Deposit Date: May 20, 2020
• Publicly Available Date: Jul 6, 2020
• Publisher: Association for Computing Machinery (ACM)
• Pages: 67-73
• Book Title: LICS '20: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science
• ISBN: 9781450371049
• DOI: https://doi.org/10.1145/3373718.3394760
• Public URL: https://nottingham-repository.worktribe.com/output/4475508
• Publisher URL: https://dl.acm.org/doi/10.1145/3373718.3394760
• Related Public URLs: http://lics.siglog.org/lics20/