Contents

Idea

The integers as familiar from school mathematics.

Definitions

The type of integers, denoted $\mathbb{Z}$, has several definitions as a higher inductive type.

Definition 1

The integers are defined as the higher inductive type generated by:

• A function $inj : \mathbf{2} \times \mathbb{N} \rightarrow \mathbb{Z}$.
• An identity representing that positive and negative zero are equal: $\nu_0: inj(0, 0) = inj(1, 0)$.

Definition 2

The integers are defined as the higher inductive type generated by:

• A term $0 : \mathbb{Z}$.
• A function $s : \mathbb{Z} \to \mathbb{Z}$.
• A function $p_1 : \mathbb{Z} \to \mathbb{Z}$.
• A function $p_2 : \mathbb{Z} \to \mathbb{Z}$.
• A dependent product of identities representing that $p_1$ is a section of $s$:
  $$\sigma: \prod_{a:\mathbb{Z}} p_1(s(a)) = a$$
• A dependent product of identities representing that $p_2$ is a retracion of $s$:
  $$\rho: \prod_{a:\mathbb{Z}} s(p_2(a)) = a$$

Definition 3

The integers are defined as the higher inductive type generated by:

• A term $0 : \mathbb{Z}$.
• A function $s : \mathbb{Z} \to \mathbb{Z}$.
• A function $p : \mathbb{Z} \to \mathbb{Z}$.
• A dependent product of identities representing that $p$ is a section of $s$:
  $$\sigma: \prod_{a:\mathbb{Z}} p(s(a)) = a$$
• A dependent product of identities representing that $p$ is a retracion of $s$:
  $$\rho: \prod_{a:\mathbb{Z}} s(p(a)) = a$$
• A dependent product of identities representing the coherence condition:
  $$\kappa: \prod_{a:\mathbb{Z}} ap_s(\sigma(a)) = \rho(a)$$

Definition 4

The integers are defined as the higher inductive type generated by:

• A term $0 : \mathbb{Z}$.
• A function $s : \mathbb{Z} \to \mathbb{Z}$.
• A function $n : \mathbb{Z} \to \mathbb{Z}$.
• An identity representing that zero and negative zero are equal: $\nu: n(0) = 0$.
• A dependent product of identities representing that negation is an involution:
  $$\iota: \prod_{a:\mathbb{Z}} n(n(a)) = a$$
• A dependent product of identities representing the coherence condition for the above:
  $$\kappa_\iota: \prod_{a:\mathbb{Z}} ap_n(\iota(a)) = \iota(a)$$
• A dependent product of identities representing that $n \circ s \circ n$ is a section of $s$:
  $$\sigma: \prod_{a:\mathbb{Z}} n(s(n(s(a)))) = a$$
• A dependent product of identities representing that $n \circ s \circ n$ is a retracion of $s$:
  $$\rho: \prod_{a:\mathbb{Z}} s(n(s(n(a)))) = a$$
• A dependent product of identities representing the coherence condition:
  $$\kappa: \prod_{a:\mathbb{Z}} ap_s(\sigma(a)) = \rho(a)$$

Definition 5

The integers are defined as the higher inductive type generated by:

• A function $inj : \mathbb{N} \times \mathbb{N} \rightarrow \mathbb{Z}$.
• A dependent product of functions between identities representing that equivalent differences are equal:
  $$equivdiff : \prod_{a:\mathbb{N}} \prod_{b:\mathbb{N}} \prod_{c:\mathbb{N}} \prod_{d:\mathbb{N}} (a + d = c + b) \to (inj(a,b) = inj(c,d))$$
• A set-truncator
  $$\tau_0: \prod_{a:\mathbb{Z}} \prod_{b:\mathbb{Z}} isProp(a=b)$$

Properties

TODO: Show that the integers are a ordered Heyting integral domain with decidable equality, decidable apartness, and decidable linear order, and that the integers are initial in the category of ordered Heyting integral domains.

See also

• higher inductive type
• rational numbers
• decimal numbers

References

HoTT book

• Thorsten Altinkirch, The Integers as a Higher Inductive Type, (abs:2007.00167)

• Marc Bezem, Ulrik Buchholtz, Pierre Cagne, Bjørn Ian Dundas, Daniel R. Grayson, Symmetry, (pdf)