The Integers as a Higher Inductive Type

How to define the integers in Homotopy Type Theory? This can sound like a trivial question. The first answer is as signed natural numbers:

However, this type is very inconvenient in practice because it creates a lot of unnecessary case distinctions. Nuo [Li15] tried to prove distributivity of multiplication over addition, which resulted in a lot of cases. It is like working with normal forms only, when working with $\lambda$-terms.

Nuo shows that it is much better to work with a quotient type, representing integers as differences of natural numbers. That is, we define $\mathbb{Z}_{q}=\mathbb{N}\times\mathbb{N}/\sim$ where $(x^{+},x^{-})\sim(y^{+},y^{-})$ is defined as $x^{+}+y^{-}=y^{+}+x^{-}$ ¹¹1This is actually the definition in [Uni13].. However, this is not the end of the story. Here we use set-quotients, which can be implemented as a higher inductive type with a set-truncation constructor [Uni13, Section 6.10]. However, the set-truncation constructor implies that using its recursion principle we can only define functions into sets, which seems to be an unreasonable limitation when working in HoTT. For example, in the proof that the loop space of the circle is isomorphic to the integers [RLS13], we must map from the integers to the loop space of the circle, when we do not yet know that this will end up being a set.

We would like to have a definition of the integers which is convenient to work with (i.e., does not reduce them to normal forms) but which is not forced to be set-truncated by a set-truncation constructor. Paolo Capriotti suggested the following definition:

We add $\mathsf{succ}$ and $\mathsf{pred}$ as constructors, but then we postulate that they are inverse to each other using $\mathsf{sec}$ and $\mathsf{ret}$. At this point we could add a set-truncation but then we would suffer from the same shortcoming as the definition using a set-quotient. However, we can add just one coherence condition $\mathsf{coh}$ which should look familiar to anybody who has read the HoTT book: indeed the constructors $\mathsf{pred}$, $\mathsf{sec}$, $\mathsf{ret}$, and $\mathsf{coh}$ exactly say that $\mathsf{succ}$ is a half-adjoint equivalence [Uni13, Section 4.2]. More precisely, $\mathsf{sec}$ postulates that $\mathsf{succ}$ is a section, $\mathsf{ret}$ postulates that $\mathsf{succ}$ is a retraction, and $\mathsf{coh}$ represents the triangle identity in the definition of half-adjoint equivalence.

The question that now remains is the following. Is $\mathbb{Z}_{h}$ a correct definition of the integers, in particular is it a set with decidable equality? The strategy to prove this is to define a normalisation function into the signed integers, $\mathbb{Z}_{w}$, and show that this normalisation function, together with the obvious embedding of $\mathbb{Z}_{w}$ into $\mathbb{Z}_{h}$, forms an equivalence. It turns out that this is actually quite hard to prove, due to the presence of higher equalities, and nobody has so far been able to formally verify this.

In this paper, we follow the same idea but use a simpler definition of equivalence, namely bi-invertible maps [Uni13, Section 4.3]:

In this case we postulate that $\mathsf{succ}$ has a left inverse, given by $\mathsf{pred}_{1}$ and $\mathsf{sec}$, and a right inverse, given by $\mathsf{pred}_{2}$ and $\mathsf{ret}$. The reason why $\mathbb{Z}_{b}$ is simpler than $\mathbb{Z}_{h}$ is because it only has $0$- and $1$-dimensional constructors. The higher coherence $\mathsf{coh}$ is not needed in this case for the same reason that a $2$-dimensional constructor is not needed in the definition of bi-invertible map: having two, a priory, unrelated inverses makes the type of witnesses that a certain map is bi-invertible a proposition ([Uni13, Theorem 4.3.2]).

For this definition we can give a complete proof that $\mathbb{Z}_{b}$ is equivalent to $\mathbb{Z}_{w}$, which has been formalized in cubical Agda. We remark that this has previously been verified by Evan Cavallo [Cav18] in RedTT [red19]. However, our approach to prove the equivalence is more general. Our main result is Theorem 2.4, which says that only the components witnessing the preservation of $0$ and $\mathsf{succ}$ are relevant when comparing morphisms out of $\mathbb{Z}_{b}$.

Another presentation of the integers follows from directly implementing the idea that the integers can be specified as the initial type with an inhabitant and an equivalence:

• –

  $0:\mathbb{Z}_{U}$;

• –

  $s:\mathbb{Z}_{U}=\mathbb{Z}_{U}$.

The problem is that this is not a standard definition of a higher inductive type because we state an equality of the type itself. However, this can be fixed by using a small universe:

While we can show that this is a set without using set-truncation, its recursion principle isn’t directly amenable to recursive definitions of functions because even $\mathsf{succ}$ is not a constructor. On the other hand the fact that the integers are the loop space of the circle is a rather easy consequence of this definition.

The definition of the integers is also closely related to the free group, indeed as suggested in [KA18] we can define the free group over a type $A$ by simply parametrizing all the constructors but $0$:

The integers arise as the special case $\mathbb{Z}=\mathbf{F}(\mathbf{1})$. However, the normal forms get a bit more complicated because we must allow alternating sequences of $\mathsf{succ}$ and $\mathsf{pred}$ but only for different $a:A$. This means that a normalisation function is only definable for sets $a:A$ with a decidable equality. The general problem of whether $\mathbf{F}(A)$ is a set, if $A$ is, is still open — in [KA18] it is shown to be the case, if we $1$-truncate the HIT.

The problem of defining the integers with convenient constructors, and adding only the right coherences to make it a set, can be seen as a simple instance of a more general class of coherence problems in HoTT. Another example that we have in mind is the intrinsic definition of the syntax of type theory as the initial category with families as developed in [AK16]. If we carry out this definition in HoTT, we need to set-truncate the syntax, but this stops us from interpreting the syntax in the standard model formed by sets. We hope that also in this case we can add the correct coherence laws and show that they are sufficient to deduce that the initial algebra is a set.

The type $\mathbb{N}$ of natural numbers is usually defined as the inductive type generated by an inhabitant $0:\mathbb{N}$ and an endomap $\mathsf{succ}:\mathbb{N}\to\mathbb{N}$. In this section, we define the integers $\mathbb{Z}_{b}$ in a similar way. The idea is to give constructors that guarantee that we have $0:\mathbb{Z}_{b}$, $\mathsf{succ}:\mathbb{Z}_{b}\to\mathbb{Z}_{b}$, and that $\mathsf{succ}$ is an equivalence using bi-invertible maps, see Definition 1.3. To make it easy to work with this definition, we prove three theorems that let us: map out of $\mathbb{Z}_{b}$ (Proposition 2.1), prove properties about $\mathbb{Z}_{b}$ (Proposition 2.2), and recognise when two maps out of $\mathbb{Z}_{b}$ are equal (Theorem 2.4).

The result about mapping out of $\mathbb{Z}_{b}$ is very simple, and follows immediately from the recursion principle of $\mathbb{Z}_{b}$.

The next result is only slightly more involved.

The result that allows us to compare maps out of $\mathbb{Z}_{b}$ is considerably more complicated to prove. In order to explain its proof, we need to talk about bi-invertible maps.

Whenever we have $f:A\simeq_{b}B$, we will abuse notation, and write $f:A\to B$ for the underlying function of the bi-invertible map $f$.

Notice that the constructors $\mathsf{succ}$, $\mathsf{pred}_{1}$, $\mathsf{pred}_{2}$, $\mathsf{sec}$, and $\mathsf{ret}$ form a bi-invertible map. Suppose given a type $T$ with an inhabitant $t:T$ and a bi-invertible map $s:T\simeq_{b}T$. The recursion principle of $\mathbb{Z}_{b}$ gives us $\mathsf{rec}_{\mathbb{Z}_{b}}(T,t,s):\mathbb{Z}_{b}\to T$. Now, assume given another map $f:\mathbb{Z}_{b}\to T$. What do we have to check to be able to conclude that $f=\mathsf{rec}_{\mathbb{Z}_{b}}(T,t,s)$?

The following theorem gives a simple answer to the question and is the main focus of this section.

In order to prove Theorem 2.4 we must study the preservation of bi-invertible maps, which we introduce next.

Fix types $A,B,A^{\prime},B^{\prime}:\mathcal{U}$, bi-invertible maps $e:A\simeq_{b}B$ and $e^{\prime}:A^{\prime}\simeq_{b}B^{\prime}$, and maps $\alpha:A\to A^{\prime}$ and $\beta:B\to B^{\prime}$:

We now define what it means for $\alpha$ and $\beta$ to respect $e$ and $e^{\prime}$. By a slight abuse of notation, let the bi-invertible maps $e$ and $e^{\prime}$ be given by $(e,g,h,s,r)$ and $(e^{\prime},g^{\prime},h^{\prime},s^{\prime},r^{\prime})$.

The next proposition follows from the initiality of $\mathbb{Z}_{b}$, although it is a bit involved to prove formally using the constructors and the induction principle.

Given a type $A:\mathcal{U}$, let $\mathsf{id}_{A}:A\to A$ be the identity function. We have $\mathsf{idb}_{A}:\mathsf{isBiInv}(\mathsf{id}_{A})$, so we can define a map $\mathsf{toBiInv}:A=B\to A\simeq_{b}B$ by path induction, sending $\mathsf{refl}:A=A$ to $\mathsf{idb}_{A}$. By [Uni13, Corollary 4.3.3] and the univalence axiom, the map $\mathsf{toBiInv}$ is an equivalence. Let $\mathsf{toEq}:A\simeq_{b}B\to A=B$ be its inverse.

From this we can derive the principle of (based) equivalence induction, which we now state.

Using equivalence induction, and singleton elimination, one can finally prove that a map between types together with bi-invertible maps that respects the maps, automatically respects the bi-invertible structure.

One should notice that Lemma 2.8 can be proven directly, avoiding the usage of the univalence axiom (which was used to prove that $\mathsf{toBiInv}$ is an equivalence). The reason why we don’t do this, is because the path algebra involved in proving Lemma 2.8 directly is non-trivial.

In this section we relate $\mathbb{Z}_{b}$ with the usual definition of the integers as signed natural numbers, which we call $\mathbb{Z}_{w}$. We show that $\mathbb{Z}_{b}\simeq\mathbb{Z}_{w}$, and since we already know that $\mathbb{Z}_{w}$ is a set, we deduce that $\mathbb{Z}_{b}$ is a set too.

In this section we give another definition of the integers, denoted by $\mathbb{Z}_{U}$, which allows one to easily prove that they are the initial type together with an inhabitant and an equality from the type to itself.

To make sense of initiality, we first define the type of $\mathbb{Z}$-algebras and of $\mathbb{Z}$-algebra morphisms.

We are interested in initial $\mathbb{Z}$-algebras.

See Definition 1.4 for the definition of the initial $\mathbb{Z}$-algebra using a mini universe²²2This is inspired by Zongpu Xie’s proposal how to represent HIITs in Agda [Kap19].. Then define an interpretation function $\mathsf{El}:U\to\mathcal{U}$, as the higher inductive family with only one constructor $0:\mathsf{El}(z)$. Define the type $\mathbb{Z}_{U}\vcentcolon\equiv\mathsf{El}(z)$. The type $\mathbb{Z}_{U}$ has the structure of a $\mathbb{Z}$-algebra, since we have $0:\mathbb{Z}_{U}$ and $s\vcentcolon\equiv\mathsf{ap}_{\mathsf{El}}(q):\mathbb{Z}_{U}=\mathbb{Z}_{U}$. The following result follows by a routine application of the induction principle of $\mathbb{Z}_{U}$.

In particular, we have.

Again, comparing maps out of $\mathbb{Z}_{U}$ is easy, thanks to the following theorem.

Analogously to the case of $\mathbb{Z}_{b}$, this is proven by combining the initiality of $\mathbb{Z}_{U}$ with the fact that to preserve an equality in the universe $e:T=T$, it is enough to commute with its corresponding coercion function $e_{*}:T\to T$.

Following the argument given in Section 3, one deduces the following.

We omit the proof since it is basically the same as the construction presented in [RLS13] when proving that the integers are the loop space of the circle.

Indeed, the mini universe $U$ is nothing but the higher inductive type presentation of the circle $S^{1}$ of [Uni13, Section 6.1], so that $(z=z)\equiv\Omega S^{1}$. Moreover, the type family $\mathsf{El}$ is equivalent to the path space fibration of the circle, in the following sense.

As a corollary, we obtain the well-known equivalence between the loop space of the circle and the integers.

This suggests that alternatively one could view the representation of the integers as a universe as an inductive-inductive presentation of the circle equipped with a family that has a point in the fiber over the base point.

We formally checked the results of this paper [AS19] using cubical Agda [AMV19]. There are two differences between the informal presentation in the paper and the formalisation. The first one is that the presentation in the paper is done using book-HoTT [Uni13], whereas the formalisation is done using a cubical type theory. In this case, this difference is not important, since it is easy to translate the formalized arguments to book-HoTT.

The real difference is in the definition of higher inductive types. In the paper we define higher inductive types as initial algebras for a certain signature (Section 1.3). In the formalisation, we use higher inductive types as implemented in cubical Agda, which are based on [CHM18]. Although it is natural to assume that the Agda higher inductive type should be initial in the sense of Section 1.3, proving this fact is actually one of the main difficulties in the formalisation (Proposition 2.6).

In proving the results of Section 2, we developed the theory of bi-invertible maps in cubical Agda, which wasn’t available. We prove that the type of bi-invertible maps between $A$ and $B$ is equivalent to the type of equivalences between $A$ and $B$, and the principle of bi-invertible induction.