@misc{indiciae7654548064d0, title = {The Integers as a Higher Inductive Type}, author = {Thorsten Altenkirch and Luis Scoccola}, year = {2020}, url = {https://arxiv.org/abs/2007.00167}, note = {Source identifier: 2007.00167} }