Showing changes from revision #3 to #4: Added | Removed | Changed

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 that the above coherence type condition is for contractible: the above:
  $${\mathrm{<span><del\; class="diffmod">\; c</del><ins\; class="diffmod">\; \kappa </ins></span>}}_{\iota }:\prod _{b:\prod _{a:\mathbb{Z}}n(n(a<span><del\; class="diffmod">\; )</del><ins\; class="diffmod">\; :</ins></span>)\mathbb{Z}=a}{\mathrm{ap}}_n(\iota (a))=\mathrm{<span><del\; class="diffmod">\; b</del><ins\; class="diffmod">\; \iota </ins></span>}(a)$$ c_\iota: \kappa_\iota: \prod_{b:\prod_{a:\mathbb{Z}} \prod_{a:\mathbb{Z}} n(n(a)) ap_n(\iota(a)) = a} \iota(a) \iota = b
• 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 Heyting ordered integral domain with decidable equality, decidable apartness, and decidable linear order, and that the integers are initial in the category of Heyting ordered integral domain.

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)