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.

Commutative ring structure on the integers

We assume in this section that the integers are defined according to definition 1.

Pseudolattice structure on the integerss

See also

• higher inductive type
• rational numbers
• decimal numbers
• Eudoxus real 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)