The Integers as a Higher Inductive Type
(2020)
Presentation / Conference Contribution
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
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... Read More about The Integers as a Higher Inductive Type.