The Integers as a Higher Inductive Type

Thorsten Altenkirch, Luis Scoccola

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 ind…