The Integers as a Higher Inductive Type

TL;DR

This paper introduces a novel higher inductive type for integers in Homotopy Type Theory, avoiding set-truncation issues and enabling more coherent representations, with formal verification in cubical Agda.

Contribution

It presents a new higher inductive type for integers in HoTT that circumvents set-truncation limitations and demonstrates handling coherence problems.

Findings

Higher inductive types can represent integers without set-truncation.

The new approach simplifies induction principles for integers in HoTT.

Formal proofs are verified in cubical Agda.

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.