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