nLab integers type

Idea

In type theory: the integers type is the type of integers.

Definitions

As the inductive type generated by an element and an equivalence of types

Assuming that identification types, equivalence types and dependent product types exist in the type theory, the integers type is the inductive type generated by an element and an equivalence of types:

Formation rules for the integers type:

$$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathbb{Z} \; \mathrm{type}}$$

Introduction rules for the integers type:

$$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash 0:\mathbb{Z}} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash s:\mathbb{Z} \simeq \mathbb{Z}}$$

Elimination rules for the integers type:

$$\frac{\Gamma, x:\mathbb{Z} \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_0:C(0) \quad \Gamma \vdash c_s:\prod_{x:\mathbb{Z}} C(x) \simeq C(s(x)) \quad \Gamma \vdash n:\mathbb{Z}}{\Gamma \vdash \mathrm{ind}_\mathbb{Z}^C(c_0, c_s, n):C(n)}$$

Computation rules for the integers type:

• Judgmental computation rules

$$\frac{\Gamma, x:\mathbb{Z} \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_0:C(0) \quad \Gamma \vdash c_s:\prod_{x:\mathbb{Z}} C(x) \simeq C(s(x))}{\Gamma \vdash \mathrm{ind}_\mathbb{Z}^C(c_0, c_s, 0) \equiv c_0:C(0)}$$

$$\frac{\Gamma, x:\mathbb{Z} \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_0:C(0) \quad \Gamma \vdash c_s:\prod_{x:\mathbb{Z}} C(x) \simeq C(s(x)) \quad \Gamma \vdash n:\mathbb{Z}}{\Gamma \vdash \mathrm{ind}_\mathbb{Z}^C(c_0, c_s, s(n)) \equiv c_s(n)(\mathrm{ind}_\mathbb{Z}^C(c_0, c_s, n)):C(s(n))}$$

• Typal computation rules

$$\frac{\Gamma, x:\mathbb{Z} \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_0:C(0) \quad \Gamma \vdash c_s:\prod_{x:\mathbb{Z}} C(x) \simeq C(s(x))}{\Gamma \vdash \beta_\mathbb{Z}^0(c_0, c_s):\mathrm{Id}_{C(0)}(\mathrm{ind}_\mathbb{Z}^C(c_0, c_s, 0), c_0)}$$

$$\frac{\Gamma, x:\mathbb{Z} \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_0:C(0) \quad \Gamma \vdash c_s:\prod_{x:\mathbb{Z}} C(x) \simeq C(s(x)) \quad \Gamma \vdash n:\mathbb{Z}}{\Gamma \vdash \beta_\mathbb{Z}^s(c_0, c_s, n):\mathrm{Id}_{C(s(n))}(\mathrm{ind}_\mathbb{Z}^C(c_0, c_s, s(n)), c_s(n)(\mathrm{ind}_\mathbb{Z}^C(c_0, c_s, n)))}$$

Uniqueness rules for the integers type:

• Judgmental uniqueness rules

$$\frac{\Gamma, x:\mathbb{Z} \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c:\prod_{x:\mathbb{Z}} C(x) \quad \Gamma \vdash n:\mathbb{Z}}{\Gamma \vdash \mathrm{ind}_\mathbb{Z}^C(c(0), \lambda x:\mathbb{Z}.c(s(x)), n) \equiv c(n):C(n)}$$

• Typal uniqueness rules

$$\frac{\Gamma, x:\mathbb{Z} \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c:\prod_{x:\mathbb{Z}} C(x) \quad \Gamma \vdash n:\mathbb{Z}}{\Gamma \vdash \eta_\mathbb{Z}(c, n):\mathrm{Id}_{C(n)}(\mathrm{ind}_\mathbb{Z}^C(c(0), \lambda x:\mathbb{Z}.c(s(x)), n), c(n))}$$

The elimination, computation, and uniqueness rules for the integers type state that the integers type satisfy the dependent universal property of the integers. If the dependent type theory also has dependent sum types and product types, allowing one to define the uniqueness quantifier, the dependent universal property of the integers could be simplified to the following rule:

$$\frac{\Gamma, x:\mathbb{Z} \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_0:C(0) \quad \Gamma \vdash c_s:\prod_{x:\mathbb{Z}} C(x) \simeq C(s(x))}{\Gamma \vdash \mathrm{up}_\mathbb{Z}^C(c_0, c_s):\exists!c:\prod_{x:\mathbb{Z}} C(x).\mathrm{Id}_{C(0)}(c(0), c_0) \times \prod_{x:\mathbb{Z}} \mathrm{Id}_{C(s(x))}(c(s(x)), c_s(c(x)))}$$

As the underlying type of the free infinity-group on the unit type

The integers type is the underlying type of free infinity-group on the unit type

$$\mathbb{Z} \coloneqq \mathrm{UnderlyingTypeOfFree}\infty\mathrm{Group}(\mathbb{1})$$

As the loop space of the circle type

Given a dependent type theory with identity types, equivalence types, a univalent universe, and the circle type which is an essentially small type relative to the universe universe, the type of integers is defined as the loop space type of the circle type at the canonical element $\mathrm{base}:S^1$:

$$\mathbb{Z} \coloneqq \mathrm{base} =_{S^1} \mathrm{base}$$

As a quotient of a product type

Definition

The integers type is 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

The integers type is 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

We assume in this section that the integers type is defined as the inductive type generated by an element and an equivalence of types.

Extensionality principle of the integers type

By the recursion principle of the natural numbers, there is a function

$$\mathrm{rec}_{\mathbb{N}}(0, \pi_1(s)):\mathbb{N} \to \mathbb{Z}$$

which takes zero of the natural numbers to zero of the integers and the successor function of the natural numbrers to the successor equivalence of the integers, where $\pi_1$ is the first projection function of the dependent sum type $\sum_{f:\mathbb{Z} \to \mathbb{Z}} \mathrm{isEquiv}(f)$. The extensionality principle of the circle type states that the above function is an embedding of types,

$$\mathrm{ext}_{S^1}:\mathrm{isEmbed}\left(\mathrm{rec}_{\mathbb{N}}(0, \pi_1(s))\right)$$

or equivalently that application of the above function is an equivalence for all natural numbers $m:\mathbb{N}$, $n:\mathbb{N}$

$$\mathrm{ext}_{S^1}:\prod_{m:\mathbb{N}} \prod_{n:\mathbb{N}} \mathrm{isEquiv}\left(\mathrm{ap}_{\mathrm{rec}_{\mathbb{N}}(0, \pi_1(s))}(m, n)\right)$$

Theorem

The integers type has decidable equality.

Proof

…

Double induction

From the inference rules for the integers type, one could derive the following rules for double induction, which is important for the definition of addition, subtraction, and multiplication on the integers:

$$\frac{ \begin{array}{c} \Gamma, x:\mathbb{Z}, y:\mathbb{Z} \vdash C(x, y) \; \mathrm{type} \quad \Gamma \vdash c_{0, 0}:C(0, 0) \quad \Gamma \vdash c_{0, s}:\prod_{x:\mathbb{Z}} C(0, x) \simeq C(0, s(x)) \\ \Gamma \vdash c_{s, 0}:\prod_{x:\mathbb{Z}} C(x, 0) \simeq C(s(x), 0) \quad \Gamma \vdash c_{s, s}:\prod_{x:\mathbb{Z}} \prod_{y:\mathbb{Z}} C(x, y) \simeq C(s(x), s(y)) \end{array} }{\Gamma \vdash \mathrm{ind}_\mathbb{Z}^C(c_{0, 0}, c_{0, s}, c_{s, 0}, c_{s, s}):\prod_{m:\mathbb{Z}} \prod_{n:\mathbb{Z}} C(m, n)}$$

$$\frac{ \begin{array}{c} \Gamma, x:\mathbb{Z}, y:\mathbb{Z} \vdash C(x, y) \; \mathrm{type} \quad \Gamma \vdash c_{0, 0}:C(0, 0) \quad \Gamma \vdash c_{0, s}:\prod_{x:\mathbb{Z}} C(0, x) \simeq C(0, s(x)) \\ \Gamma \vdash c_{s, 0}:\prod_{x:\mathbb{Z}} C(x, 0) \simeq C(s(x), 0) \quad \Gamma \vdash c_{s, s}:\prod_{x:\mathbb{Z}} \prod_{y:\mathbb{Z}} C(x, y) \simeq C(s(x), s(y)) \end{array} }{\Gamma \vdash \beta_\mathbb{Z}^{C, 0, 0}(c_{0, 0}, c_{0, s}, c_{s, 0}, c_{s, s}):\mathrm{ind}_\mathbb{Z}^C(c_{0, 0}, c_{0, s}, c_{s, 0}, c_{s, s}, 0, 0) =_{C(0, 0)} c_{0, 0}}$$

$$\frac{ \begin{array}{c} \Gamma, x:\mathbb{Z}, y:\mathbb{Z} \vdash C(x, y) \; \mathrm{type} \quad \Gamma \vdash c_{0, 0}:C(0, 0) \quad \Gamma \vdash c_{0, s}:\prod_{x:\mathbb{Z}} C(0, x) \simeq C(0, s(x)) \\ \Gamma \vdash c_{s, 0}:\prod_{x:\mathbb{Z}} C(x, 0) \simeq C(s(x), 0) \quad \Gamma \vdash c_{s, s}:\prod_{x:\mathbb{Z}} \prod_{y:\mathbb{Z}} C(x, y) \simeq C(s(x), s(y)) \end{array} }{\Gamma \vdash \beta_\mathbb{Z}^{C, 0, s}(c_{0, 0}, c_{0, s}, c_{s, 0}, c_{s, s}):\prod_{n:\mathbb{Z}} \mathrm{ind}_\mathbb{Z}^C(c_{0, 0}, c_{0, s}, c_{s, 0}, c_{s, s}, 0, s(n)) =_{C(0, s(n))} c_{0, s}(n, \mathrm{ind}_\mathbb{Z}^C(c_{0, 0}, c_{0, s}, c_{s, 0}, c_{s, s}, 0, n))}$$

$$\frac{ \begin{array}{c} \Gamma, x:\mathbb{Z}, y:\mathbb{Z} \vdash C(x, y) \; \mathrm{type} \quad \Gamma \vdash c_{0, 0}:C(0, 0) \quad \Gamma \vdash c_{0, s}:\prod_{x:\mathbb{Z}} C(0, x) \simeq C(0, s(x)) \\ \Gamma \vdash c_{s, 0}:\prod_{x:\mathbb{Z}} C(x, 0) \simeq C(s(x), 0) \quad \Gamma \vdash c_{s, s}:\prod_{x:\mathbb{Z}} \prod_{y:\mathbb{Z}} C(x, y) \simeq C(s(x), s(y)) \end{array} }{\Gamma \vdash \beta_\mathbb{Z}^{C, s, 0}(c_{0, 0}, c_{0, s}, c_{s, 0}, c_{s, s}):\prod_{n:\mathbb{Z}} \mathrm{ind}_\mathbb{Z}^C(c_{0, 0}, c_{0, s}, c_{s, 0}, c_{s, s}, s(n), 0) =_{C(s(n), 0)} c_{s, 0}(n, \mathrm{ind}_\mathbb{Z}^C(c_{0, 0}, c_{0, s}, c_{s, 0}, c_{s, s}, n, 0))}$$

$$\frac{ \begin{array}{c} \Gamma, x:\mathbb{Z}, y:\mathbb{Z} \vdash C(x, y) \; \mathrm{type} \quad \Gamma \vdash c_{0, 0}:C(0, 0) \quad \Gamma \vdash c_{0, s}:\prod_{x:\mathbb{Z}} C(0, x) \simeq C(0, s(x)) \\ \Gamma \vdash c_{s, 0}:\prod_{x:\mathbb{Z}} C(x, 0) \simeq C(s(x), 0) \quad \Gamma \vdash c_{s, s}:\prod_{x:\mathbb{Z}} \prod_{y:\mathbb{Z}} C(x, y) \simeq C(s(x), s(y)) \end{array} }{\Gamma \vdash \beta_\mathbb{Z}^{C, s, s}(c_{0, 0}, c_{0, s}, c_{s, 0}, c_{s, s}):\prod_{m:\mathbb{Z}} \prod_{n:\mathbb{Z}} \mathrm{ind}_\mathbb{Z}^C(c_{0, 0}, c_{0, s}, c_{s, 0}, c_{s, s}, s(m), s(n)) =_{C(s(m), s(n))} c_{0, s}(m, n, \mathrm{ind}_\mathbb{Z}^C(c_{0, 0}, c_{0, s}, c_{s, 0}, c_{s, s}, m, n))}$$

Addition on the integers

Definition

The binary operation addition is defined by double induction, where the type family $C$ is the constant type family $\mathbb{Z}$, $c_{0, 0}$ is $0$, $c_{0, s}$ and $c_{s, 0}$ are both the constant function $\lambda n:\mathbb{Z}.s$ which takes integers to the successor equivalence, and $c_{s, s}$ is the constant function $\lambda m:\mathbb{Z}.\lambda n:\mathbb{Z}.s \circ s$ which takes pairs of integers to the composition of the successor equivalence with itself, and is defined pointwise as

$$x:\mathbb{Z}, y:\mathbb{Z} \vdash x + y \equiv \mathrm{ind}_\mathbb{Z}^\mathbb{Z}(0, \lambda n:\mathbb{Z}.s, \lambda n:\mathbb{Z}.s, \lambda m:\mathbb{Z}.\lambda n:\mathbb{Z}.s \circ s, x, y):\mathbb{Z}$$

We have similar definitions for the computation rules of addition:

$$\beta_\mathbb{Z}^{+, 0, 0} \equiv \beta_\mathbb{Z}^{\mathbb{Z}, 0, 0}(0, \lambda n:\mathbb{Z}.s, \lambda n:\mathbb{Z}.s, \lambda m:\mathbb{Z}.\lambda n:\mathbb{Z}.s \circ s):0 + 0 =_{\mathbb{Z}} 0$$

$$\beta_\mathbb{Z}^{+, 0, s} \equiv \beta_\mathbb{Z}^{\mathbb{Z}, 0, s}(0, \lambda n:\mathbb{Z}.s, \lambda n:\mathbb{Z}.s, \lambda m:\mathbb{Z}.\lambda n:\mathbb{Z}.s \circ s):\prod_{x:\mathbb{Z}} 0 + s(x) =_{\mathbb{Z}} ((\lambda n:\mathbb{Z}.s)(x))(0 + x)$$

$$\beta_\mathbb{Z}^{+, s, 0} \equiv \beta_\mathbb{Z}^{\mathbb{Z}, s, 0}(0, \lambda n:\mathbb{Z}.s, \lambda n:\mathbb{Z}.s, \lambda m:\mathbb{Z}.\lambda n:\mathbb{Z}.s \circ s):\prod_{x:\mathbb{Z}} s(x) + 0 =_{\mathbb{Z}} ((\lambda n:\mathbb{Z}.s)(x))(x + 0)$$

$$\beta_\mathbb{Z}^{+, s, s} \equiv \beta_\mathbb{Z}^{\mathbb{Z}, s, s}(0, \lambda n:\mathbb{Z}.s, \lambda n:\mathbb{Z}.s, \lambda m:\mathbb{Z}.\lambda n:\mathbb{Z}.s \circ s):\prod_{x:\mathbb{Z}} \prod_{y:\mathbb{Z}} s(x) + s(y) =_{\mathbb{Z}} ((\lambda m:\mathbb{Z}.\lambda n:\mathbb{Z}.s \circ s)(x, y))(x + y)$$

Theorem

The integers type is a non-coherent H-space with respect to the zero integer $0:\mathbb{Z}$ found in the introduction rule of the integers type and addition $x:\mathbb{Z}, y:\mathbb{Z} \vdash x + y:\mathbb{Z}$ defined above.

Proof

We define the homotopies for the H-space structure of the integers type by induction on the integers type. For the case with the element $0:\mathbb{Z}$, one gets the identity $\beta_\mathbb{Z}^{+, 0, 0}:0 + 0 =_\mathbb{Z} 0$ from the rules for addition. For the case with the equivalence $s:\mathbb{Z} \simeq \mathbb{Z}$, the application to $s$ is itself a dependent function of a family of equivalences,

$$\mathrm{ap}_{s}:\prod_{y:\mathbb{Z}} \prod_{x:\mathbb{Z}} (y =_\mathbb{Z} x) \simeq (s(y) =_\mathbb{Z} s(x))$$

Substituting $0 + x$ and $x + 0$ in for $y$ yields the family of equivalences

$$x:\mathbb{Z} \vdash \mathrm{ap}_{s}(0 + x, x):(0 + x =_\mathbb{Z} x) \simeq (s(0 + x) =_\mathbb{Z} s(x))$$

$$x:\mathbb{Z} \vdash \mathrm{ap}_{s}(x + 0, x):(x + 0 =_\mathbb{Z} x) \simeq (s(x + 0) =_\mathbb{Z} s(x))$$

and by the introduction rule of dependent product types, one gets the dependent functions of families of equivalences

$$\lambda x:\mathbb{Z}.\mathrm{ap}_{s}(0 + x, x):\prod_{x:\mathbb{Z}} (0 + x =_\mathbb{Z} x) \simeq (s(0 + x) =_\mathbb{Z} s(x))$$

$$\lambda x:\mathbb{Z}.\mathrm{ap}_{s}(x + 0, x):\prod_{x:\mathbb{Z}} (x + 0 =_\mathbb{Z} x) \simeq (s(x + 0) =_\mathbb{Z} s(x))$$

and by the elimination rules for the integers type, one has families of identifications

$$x:\mathbb{Z} \vdash \mathrm{ind}_\mathbb{Z}^{0 + x =_\mathbb{Z} x}(\beta_\mathbb{Z}^{+, 0, 0}, \lambda x:\mathbb{Z}.\mathrm{ap}_{s}(0 + x, x), x):0 + x =_\mathbb{Z} x$$

$$x:\mathbb{Z} \vdash \mathrm{ind}_\mathbb{Z}^{x + 0 =_\mathbb{Z} x}(\beta_\mathbb{Z}^{+, 0, 0}, \lambda x:\mathbb{Z}.\mathrm{ap}_{s}(x + 0, x), x):x + 0 =_\mathbb{Z} x$$

By the introduction rule of dependent product types, one gets homotopies

$$\mathrm{lunitadd}_\mathbb{Z} \equiv \lambda x:\mathbb{Z}.\mathrm{ind}_\mathbb{Z}^{0 + x =_\mathbb{Z} x}(\beta_\mathbb{Z}^{+, 0, 0}, \lambda x:\mathbb{Z}.\mathrm{ap}_{s}(0 + x, x), x):\prod_{x:\mathbb{Z}} 0 + x =_\mathbb{Z} x$$

$$\mathrm{runitadd}_\mathbb{Z} \equiv \lambda x:\mathbb{Z}.\mathrm{ind}_\mathbb{Z}^{x + 0 =_\mathbb{Z} x}(\beta_\mathbb{Z}^{+, 0, 0}, \lambda x:\mathbb{Z}.\mathrm{ap}_{s}(x + 0, x), x):\prod_{x:\mathbb{Z}} x + 0 =_\mathbb{Z} x$$

Thus, the integers type is a non-coherent H-space.

Theorem

The integers type is an associative non-coherent H-space.

Proof

…

Theorem

The integers type is invertible with respect to the H-space structure of addition - such that given an integer $x:\mathbb{Z}$, left addition and right addition by $x$ is each an equivalence of types.

Proof

…

Corollary

The integers type is a non-coherent H-group, a non-coherent H-space which is invertible and associative.

Theorem

The integers type is non-coherently abelian with respect to addition.

Proof

…

Negation on the integers

Definition

The unary operation negation is defined by induction on the integers type, where the type family $C$ is the constant type family $\mathbb{Z}$, $c_{0}$ is $0$, and $c_{s}$ is the constant function $\lambda n:\mathbb{Z}.s^{-1}$ which takes integers to the inverse of the successor equivalence, and is defined pointwise as

$$x:\mathbb{Z} \vdash -x \equiv \mathrm{ind}_\mathbb{Z}^\mathbb{Z}(0, \lambda n:\mathbb{Z}.s^{-1}, x):\mathbb{Z}$$

We have similar definitions for the computation rules of negation:

$$\beta_\mathbb{Z}^{-, 0} \equiv \beta_\mathbb{Z}^{\mathbb{Z}, 0}(0, \lambda n:\mathbb{Z}.s^{-1}):-0 =_{\mathbb{Z}} 0$$

$$\beta_\mathbb{Z}^{-, s} \equiv \beta_\mathbb{Z}^{\mathbb{Z}, s}(0, \lambda n:\mathbb{Z}.s^{-1}):\prod_{x:\mathbb{Z}} -s(x) =_{\mathbb{Z}} ((\lambda n:\mathbb{Z}.s^{-1})(x))(-x) \equiv s^{-1}(-x)$$

Subtraction on the integers

Definition

The binary operation subtraction is defined by double induction, where the type family $C$ is the constant type family $\mathbb{Z}$, $c_{0, 0}$ is $0$, $c_{0, s}$ is the constant function $\lambda n:\mathbb{Z}.s^{-1}$ which takes integers to the inverse of the successor equivalence, $c_{s, 0}$ is the constant function $\lambda n:\mathbb{Z}.s$ which takes integers to the successor equivalence, and $c_{s, s}$ is the constant function $\lambda m:\mathbb{Z}.\lambda n:\mathbb{Z}.\mathrm{id}_\mathbb{Z}$ which takes pairs of integers to the identity equivalence on the integers, and is defined pointwise as

$$x:\mathbb{Z}, y:\mathbb{Z} \vdash x - y \equiv \mathrm{ind}_\mathbb{Z}^\mathbb{Z}(0, \lambda n:\mathbb{Z}.s^{-1}, \lambda n:\mathbb{Z}.s, \lambda m:\mathbb{Z}.\lambda n:\mathbb{Z}.\mathrm{id}_\mathbb{Z}, x, y):\mathbb{Z}$$

We have similar definitions for the computation rules of subtraction:

$$\beta_\mathbb{Z}^{-, 0, 0} \equiv \beta_\mathbb{Z}^{\mathbb{Z}, 0, 0}(0, \lambda n:\mathbb{Z}.s^{-1}, \lambda n:\mathbb{Z}.s, \lambda m:\mathbb{Z}.\lambda n:\mathbb{Z}.\mathrm{id}_\mathbb{Z}):0 - 0 =_{\mathbb{Z}} 0$$

$$\beta_\mathbb{Z}^{-, 0, s} \equiv \beta_\mathbb{Z}^{\mathbb{Z}, 0, s}(0, \lambda n:\mathbb{Z}.s^{-1}, \lambda n:\mathbb{Z}.s, \lambda m:\mathbb{Z}.\lambda n:\mathbb{Z}.\mathrm{id}_\mathbb{Z}):\prod_{x:\mathbb{Z}} 0 - s(x) =_{\mathbb{Z}} ((\lambda n:\mathbb{Z}.s^{-1})(x))(0 - x) \equiv s^{-1}(0 - x)$$

$$\beta_\mathbb{Z}^{-, s, 0} \equiv \beta_\mathbb{Z}^{\mathbb{Z}, s, 0}(0, \lambda n:\mathbb{Z}.s^{-1}, \lambda n:\mathbb{Z}.s, \lambda m:\mathbb{Z}.\lambda n:\mathbb{Z}.\mathrm{id}_\mathbb{Z}):\prod_{x:\mathbb{Z}} s(x) - 0 =_{\mathbb{Z}} ((\lambda n:\mathbb{Z}.s)(x))(x - 0) \equiv s(x - 0)$$

$$\beta_\mathbb{Z}^{-, s, s} \equiv \beta_\mathbb{Z}^{\mathbb{Z}, s, s}(0, \lambda n:\mathbb{Z}.s^{-1}, \lambda n:\mathbb{Z}.s, \lambda m:\mathbb{Z}.\lambda n:\mathbb{Z}.\mathrm{id}_\mathbb{Z}):\prod_{x:\mathbb{Z}} \prod_{y:\mathbb{Z}} s(x) - s(y) =_{\mathbb{Z}} ((\lambda m:\mathbb{Z}.\lambda n:\mathbb{Z}.\mathrm{id}_\mathbb{Z})(x, y))(x - y) \equiv x - y$$

Theorem

For all $x:\mathbb{Z}$ and $y:\mathbb{Z}$, we have an identification of type

$$x - y =_\mathbb{Z} x + (- y)$$

Set-truncation structure

To do: figure out a way to prove that the integers type is 0-truncated without using the natural numbers type. Then we define the natural numbers type $\mathbb{N}$ as the quotient of the integers type by its group of units $\mathbb{Z}/\mathbb{Z}^\times$.

Theorem

The natural numbers type $\mathbb{N}$ is 0-truncated.

Proof

…

Theorem

The natural numbers type $\mathbb{N}$ and the integers type $\mathbb{Z}$ are equivalent to each other.

Proof

…

Corollary

The integers type are an abelian group.

Proof

Since $\mathbb{N}$ is 0-truncated, and equivalences preserve truncatedness, by the equivalence $e:\mathbb{N} \simeq \mathbb{Z}$, $\mathbb{Z}$ is also 0-truncated. Since $\mathbb{Z}$ is an non-coherently abelian H-group, this implies that $\mathbb{Z}$ is a abelian group.

Multiplication on the integers

To do: figure out a way to prove the various properties of multiplication without using the fact that the integers are a set (i.e. the integers are a non-coherently abelian H-ring).

Definition

Since the integers are a non-coherently abelian H-group with respect to addition, right addition by an integer $k$, $\lambda z:\mathbb{Z}.z + k$, is an equivalence.

The binary operation multiplication is defined by double induction, where the type family $C$ is the constant type family $\mathbb{Z}$, $c_{0, 0}$ is $0$, $c_{0, s}$ and $c_{s, 0}$ are both the constant function $\lambda n:\mathbb{Z}.\mathrm{id}_\mathbb{Z}$ which takes integers to the identity equivalence on the integers, and $c_{s, s}$ is the function $\lambda m:\mathbb{Z}.\lambda n:\mathbb{Z}.\lambda z:\mathbb{Z}.z + s(m + n)$ which takes pairs of integers to the equivalence $\lambda z:\mathbb{Z}.z + s(m + n)$, and is defined pointwise as

$$x:\mathbb{Z}, y:\mathbb{Z} \vdash x \cdot y \equiv \mathrm{ind}_\mathbb{Z}^\mathbb{Z}(0, \lambda n:\mathbb{Z}.\mathrm{id}_\mathbb{Z}, \lambda n:\mathbb{Z}.\mathrm{id}_\mathbb{Z}, \lambda m:\mathbb{Z}.\lambda m:\mathbb{Z}.\lambda n:\mathbb{Z}.\lambda z:\mathbb{Z}.z + s(m + n), x, y):\mathbb{Z}$$

We have similar definitions for the computation rules of multiplication:

$$\beta_\mathbb{Z}^{\cdot, 0, 0} \equiv \beta_\mathbb{Z}^{\mathbb{Z}, 0, 0}(0, \lambda n:\mathbb{Z}.\mathrm{id}_\mathbb{Z}, \lambda n:\mathbb{Z}.\mathrm{id}_\mathbb{Z}, \lambda m:\mathbb{Z}.\lambda m:\mathbb{Z}.\lambda n:\mathbb{Z}.\lambda z:\mathbb{Z}.z + s(m + n)):0 \cdot 0 =_{\mathbb{Z}} 0$$

$$\beta_\mathbb{Z}^{\cdot, 0, s} \equiv \beta_\mathbb{Z}^{\mathbb{Z}, 0, s}(0, \lambda n:\mathbb{Z}.\mathrm{id}_\mathbb{Z}, \lambda n:\mathbb{Z}.\mathrm{id}_\mathbb{Z}, \lambda m:\mathbb{Z}.\lambda m:\mathbb{Z}.\lambda n:\mathbb{Z}.\lambda z:\mathbb{Z}.z + s(m + n)):\prod_{x:\mathbb{Z}} 0 \cdot s(x) =_{\mathbb{Z}} ((\lambda n:\mathbb{Z}.\mathrm{id}_\mathbb{Z})(x))(0 \cdot x) \equiv 0 \cdot x$$

$$\beta_\mathbb{Z}^{\cdot, s, 0} \equiv \beta_\mathbb{Z}^{\mathbb{Z}, s, 0}(0, \lambda n:\mathbb{Z}.\mathrm{id}_\mathbb{Z}, \lambda n:\mathbb{Z}.\mathrm{id}_\mathbb{Z}, \lambda m:\mathbb{Z}.\lambda m:\mathbb{Z}.\lambda n:\mathbb{Z}.\lambda z:\mathbb{Z}.z + s(m + n)):\prod_{x:\mathbb{Z}} s(x) \cdot 0 =_{\mathbb{Z}} ((\lambda n:\mathbb{Z}.\mathrm{id}_\mathbb{Z})(x))(x \cdot 0) \equiv x \cdot 0$$

$$\beta_\mathbb{Z}^{\cdot, s, s} \equiv \beta_\mathbb{Z}^{\mathbb{Z}, s, s}(0, \lambda n:\mathbb{Z}.\mathrm{id}_\mathbb{Z}, \lambda n:\mathbb{Z}.\mathrm{id}_\mathbb{Z}, \lambda m:\mathbb{Z}.\lambda m:\mathbb{Z}.\lambda n:\mathbb{Z}.\lambda z:\mathbb{Z}.z + s(m + n)):\prod_{x:\mathbb{Z}} \prod_{y:\mathbb{Z}} s(x) \cdot s(y) =_{\mathbb{Z}} ((\lambda m:\mathbb{Z}.\lambda n:\mathbb{Z}.\lambda z:\mathbb{Z}.z + s(m + n)))(x, y))(x \cdot y) \equiv x \cdot y + s(x + y)$$

Theorem

The integers type is an absorption magma with respect to the zero integer $0:\mathbb{Z}$ and multiplication $x:\mathbb{Z}, y:\mathbb{Z} \vdash x \cdot y:\mathbb{Z}$ defined above.

Proof

We begin with the left absorption law, that $0 \cdot x =_\mathbb{Z} 0$ for all $x:\mathbb{Z}$. By the computation rules for the integers type, we have

$$\beta_\mathbb{Z}^{\cdot, 0, 0}:0 \cdot 0 =_{\mathbb{Z}} 0$$

Then we need to show that for all $x:\mathbb{Z}$ we have an equivalence

$$(0 \cdot x =_{\mathbb{Z}} 0) \simeq (0 \cdot s(x) =_{\mathbb{Z}} 0)$$

But that’s given by transport across the identification

$$\beta_\mathbb{Z}^{\cdot, 0, s}(x)^{-1}:0 \cdot x =_\mathbb{Z} 0 \cdot s(x)$$

for the type family $x =_\mathbb{Z} 0$:

$$\mathrm{transport}_{x:\mathbb{Z}.x =_\mathbb{Z} 0}(0 \cdot x, 0 \cdot s(x), \beta_\mathbb{Z}^{\cdot, 0, s}(x)^{-1}):(0 \cdot x =_{\mathbb{Z}} 0) \simeq (0 \cdot s(x) =_{\mathbb{Z}} 0)$$

Thus, by induction on the integers, we have

$$\mathrm{labsorp}_\mathbb{Z} \equiv \mathrm{ind}_\mathbb{Z}^{x:\mathbb{Z}.x \cdot 0 =_\mathbb{Z} 0}(\beta_\mathbb{Z}^{\cdot, 0, 0}, \lambda x:\mathbb{Z}.\mathrm{transport}_{x:\mathbb{Z}.x =_\mathbb{Z} 0}(0 \cdot x, 0 \cdot s(x), \beta_\mathbb{Z}^{\cdot, 0, s}(x)^{-1})):\prod_{x:\mathbb{Z}} 0 \cdot x =_\mathbb{Z} 0$$

Similarly, for the right absorption law, we have an equivalence

$$(x \cdot 0 =_{\mathbb{Z}} 0) \simeq (s(x) \cdot 0 =_{\mathbb{Z}} 0)$$

given by transport across the identification

$$\beta_\mathbb{Z}^{\cdot, s, 0}(x)^{-1}:x \cdot 0 =_\mathbb{Z} s(x) \cdot 0$$

for the type family $x =_\mathbb{Z} 0$:

$$\mathrm{transport}_{x:\mathbb{Z}.x =_\mathbb{Z} 0}(x \cdot 0, s(x) \cdot 0, \beta_\mathbb{Z}^{\cdot, s, 0}(x)^{-1}):(x \cdot 0 =_{\mathbb{Z}} 0) \simeq (s(x) \cdot 0 =_{\mathbb{Z}} 0)$$

Thus, by induction on the integers, we have

$$\mathrm{rabsorp}_\mathbb{Z} \equiv \mathrm{ind}_\mathbb{Z}^{x:\mathbb{Z}.0 \cdot x =_\mathbb{Z} 0}(\beta_\mathbb{Z}^{\cdot, 0, 0}, \lambda x:\mathbb{Z}.\mathrm{transport}_{x:\mathbb{Z}.x =_\mathbb{Z} 0}(x \cdot 0, s(x) \cdot 0, \beta_\mathbb{Z}^{\cdot, s, 0}(x)^{-1})):\prod_{x:\mathbb{Z}} x \cdot 0 =_\mathbb{Z} 0$$

Thus, the integers are an absorption magma with respect to zero and multiplication.

Theorem

Multiplication in the integers type is bilinear with respect to addition.

Proof

We begin with bilinearity in the right parameter of multiplication, and we prove by double induction on the integers: given an integer $x:\mathbb{Z}$, we need to show the following types have elements:

$$x \cdot (0 + 0) =_\mathbb{Z} x \cdot 0 + x \cdot 0$$

$$\prod_{y:\mathbb{Z}} (x \cdot (0 + y) =_\mathbb{Z} x \cdot 0 + x \cdot y) \simeq (x \cdot (0 + s(y)) =_\mathbb{Z} x \cdot 0 + x \cdot s(y))$$

$$\prod_{y:\mathbb{Z}} (x \cdot (y + 0) =_\mathbb{Z} x \cdot y + x \cdot 0) \simeq (x \cdot (s(y) + 0) =_\mathbb{Z} x \cdot s(y) + x \cdot 0)$$

$$\prod_{y:\mathbb{Z}} \prod_{z:\mathbb{Z}} (x \cdot (y + z) =_\mathbb{Z} x \cdot y + x \cdot z) \simeq (x \cdot (s(y) + s(z)) =_\mathbb{Z} x \cdot s(y) + x \cdot s(z))$$

Now, for the first type, by application of the function $\lambda z:\mathbb{Z}.x \cdot z$ on the identification $\beta_\mathbb{Z}^{+, 0, 0}:0 + 0 =_\mathbb{Z} 0$, we have

$$\mathrm{ap}_{\lambda z:\mathbb{Z}.x \cdot z}(0 + 0, 0, \beta_\mathbb{Z}^{+, 0, 0}):x \cdot (0 + 0) =_\mathbb{Z} x \cdot 0$$

Similarly, by the right absorption law of multiplication, we have

$$\mathrm{rabsorp}_\mathbb{Z}(x):x \cdot 0 =_\mathbb{Z} 0$$

and by application of the function $\lambda z:\mathbb{Z}.x \cdot 0 + z$ across $\mathrm{rabsorp}_\mathbb{Z}(x)$, we have

$$\mathrm{ap}_{\lambda z:\mathbb{Z}.x \cdot 0 + z}(x \cdot 0, 0, \mathrm{rabsorp}_\mathbb{Z}(x)):x \cdot 0 + x \cdot 0 =_\mathbb{Z} x \cdot 0 + 0$$

By the right unit law for addition, we have

$$\mathrm{runitadd}_{\mathbb{Z}}(x \cdot 0):x \cdot 0 + 0 =_{\mathbb{Z}} x \cdot 0$$

Thus, by concatenating identifications we have

$$\mathrm{rdist}_\mathbb{Z}^{0, 0}(x) \equiv \mathrm{ap}_{\lambda z:\mathbb{Z}.x \cdot z}(0 + 0, 0, \beta_\mathbb{Z}^{+, 0, 0}) \bullet \mathrm{runitadd}_{\mathbb{Z}}(x \cdot 0)^{-1} \bullet \mathrm{ap}_{\lambda z:\mathbb{Z}.x \cdot 0 + z}(x \cdot 0, 0, \mathrm{rabsorp}_\mathbb{Z}(x))^{-1}:x \cdot (0 + 0) =_\mathbb{Z} x \cdot 0 + x \cdot 0$$

Next, we need to show that for all $y:\mathbb{Z}$ there is an equivalence of types

$$(x \cdot (0 + y) =_\mathbb{Z} x \cdot 0 + x \cdot y) \simeq (x \cdot (0 + s(y)) =_\mathbb{Z} x \cdot 0 + x \cdot s(y))$$

By transport across the identification $\mathrm{rabsorp}_\mathbb{Z}(x):x \cdot 0 =_\mathbb{Z} 0$ for type families

$$x \cdot (0 + y) =_\mathbb{Z} z + x \cdot y$$

and

$$x \cdot (0 + s(y)) =_\mathbb{Z} z + x \cdot s(y)$$

we get equivalences

$$\mathrm{transport}_{z:\mathbb{Z}.x \cdot (0 + y) =_\mathbb{Z} z + x \cdot y}(x \cdot 0, 0, \mathrm{rabsorp}_\mathbb{Z}(x)):(x \cdot (0 + y) =_\mathbb{Z} x \cdot 0 + x \cdot y) \simeq (x \cdot (0 + y) =_\mathbb{Z} 0 + x \cdot y)$$

and

$$\mathrm{transport}_{z:\mathbb{Z}.x \cdot (0 + s(y)) =_\mathbb{Z} z + x \cdot s(y)}(x \cdot 0, 0, \mathrm{rabsorp}_\mathbb{Z}(x)):(x \cdot (0 + s(y)) =_\mathbb{Z} x \cdot 0 + x \cdot s(y)) \simeq (x \cdot (0 + y) =_\mathbb{Z} 0 + x \cdot s(y))$$

Similarly, by transport across the identification

$$\mathrm{lunitadd}_\mathbb{Z}(x \cdot y):0 + x \cdot y =_\mathbb{Z} x \cdot y$$

for type family

$$x \cdot (0 + y) =_\mathbb{Z} z$$

we get the equivalence

$$\mathrm{transport}_{z:\mathbb{Z}.x \cdot (0 + y) =_\mathbb{Z} z}(0 + x \cdot y, x \cdot y, \mathrm{lunitadd}_\mathbb{Z}(x \cdot y)):(x \cdot (0 + y) =_\mathbb{Z} 0 + x \cdot y) \simeq (x \cdot (0 + y) =_\mathbb{Z} x \cdot y)$$

and by transport across the identification

$$\mathrm{lunitadd}_\mathbb{Z}(x \cdot s(y)):0 + x \cdot s(y) =_\mathbb{Z} x \cdot s(y)$$

for type family

$$x \cdot (0 + s(y)) =_\mathbb{Z} z$$

we get the equivalence

$$\mathrm{transport}_{z:\mathbb{Z}.x \cdot (0 + s(y)) =_\mathbb{Z} z}(0 + x \cdot s(y), x \cdot s(y), \mathrm{lunitadd}_\mathbb{Z}(x \cdot s(y))):(x \cdot (0 + s(y)) =_\mathbb{Z} 0 + x \cdot s(y)) \simeq (x \cdot (0 + s(y)) =_\mathbb{Z} x \cdot s(y))$$

By transport across the identification

$$\mathrm{lunitadd}_\mathbb{Z}(y):0 + y =_\mathbb{Z} y$$

for type family

$$x \cdot z =_\mathbb{Z} x \cdot y$$

we get the equivalence

$$\mathrm{transport}_{z:\mathbb{Z}.x \cdot z =_\mathbb{Z} x \cdot y}(0 + y, y, \mathrm{lunitadd}_\mathbb{Z}(y)):(x \cdot (0 + y) =_\mathbb{Z} x \cdot y) \simeq (x \cdot y =_\mathbb{Z} x \cdot y)$$

and by transport across the identification

$$\mathrm{lunitadd}_\mathbb{Z}(s(y)):0 + s(y) =_\mathbb{Z} s(y)$$

for type family

$$x \cdot z =_\mathbb{Z} x \cdot s(y)$$

we get the equivalence

$$\mathrm{transport}_{z:\mathbb{Z}.x \cdot z =_\mathbb{Z} x \cdot y}(0 + s(y), s(y), \mathrm{lunitadd}_\mathbb{Z}(y)):(x \cdot (0 + s(y)) =_\mathbb{Z} x \cdot s(y)) \simeq (x \cdot s(y) =_\mathbb{Z} x \cdot s(y))$$

Thus, it remains to show that there is an equivalence

$$(x \cdot y =_\mathbb{Z} x \cdot y) \simeq (x \cdot s(y) =_\mathbb{Z} x \cdot s(y))$$

But since $\mathbb{Z}$ is a set, both identity types are propositions, and have elements $\mathrm{refl}_\mathbb{Z}(x \cdot y)$ and $\mathrm{refl}_\mathbb{Z}(x \cdot s(y))$ respectively. As a result, both identity types are contractible types, and contractible types are equivalent to each other. Thus, we have an equivalence:

$$f(x, y):(x \cdot y =_\mathbb{Z} x \cdot y) \simeq (x \cdot s(y) =_\mathbb{Z} x \cdot s(y))$$

Finally, by composing all the equivalences above, we get an equivalence

$$\begin{array}{c} \mathrm{rdist}_\mathbb{Z}^{0, s}(x, y) \equiv \mathrm{transport}_{z:\mathbb{Z}.x \cdot (0 + s(y)) =_\mathbb{Z} z + x \cdot s(y)}(x \cdot 0, 0, \mathrm{rabsorp}_\mathbb{Z}(x)) \circ \mathrm{transport}_{z:\mathbb{Z}.x \cdot (0 + s(y)) =_\mathbb{Z} z}(0 + x \cdot s(y), x \cdot s(y), \mathrm{lunitadd}_\mathbb{Z}(x \cdot s(y)))\\ \circ \mathrm{transport}_{z:\mathbb{Z}.x \cdot z =_\mathbb{Z} x \cdot y}(0 + s(y), s(y), \mathrm{lunitadd}_\mathbb{Z}(s(y))) \circ f(x, y) \\ \circ \mathrm{transport}_{z:\mathbb{Z}.x \cdot z =_\mathbb{Z} x \cdot y}(0 + y, y, \mathrm{lunitadd}_\mathbb{Z}(y)) \circ \mathrm{transport}_{z:\mathbb{Z}.x \cdot (0 + y) =_\mathbb{Z} z}(0 + x \cdot y, x \cdot y, \mathrm{lunitadd}_\mathbb{Z}(x \cdot y)) \\ \circ \mathrm{transport}_{z:\mathbb{Z}.x \cdot (0 + y) =_\mathbb{Z} z + x \cdot y}(x \cdot 0, 0, \mathrm{rabsorp}_\mathbb{Z}(x)):(x \cdot (0 + y) =_\mathbb{Z} x \cdot 0 + x \cdot y) \simeq (x \cdot (0 + s(y)) =_\mathbb{Z} x \cdot 0 + x \cdot s(y)) \end{array}$$

By a similar argument, we have

$$\begin{array}{c} \mathrm{rdist}_\mathbb{Z}^{s, 0}(x, y) \equiv \mathrm{transport}_{z:\mathbb{Z}.x \cdot (s(y) + 0) =_\mathbb{Z} x \cdot s(y) + z}(x \cdot 0, 0, \mathrm{rabsorp}_\mathbb{Z}(x)) \circ \mathrm{transport}_{z:\mathbb{Z}.x \cdot (s(y) + 0) =_\mathbb{Z} z}(x \cdot s(y) + 0, x \cdot s(y), \mathrm{runitadd}_\mathbb{Z}(x \cdot s(y)))\\ \circ \mathrm{transport}_{z:\mathbb{Z}.x \cdot z =_\mathbb{Z} x \cdot y}(s(y) + 0, s(y), \mathrm{runitadd}_\mathbb{Z}(s(y))) \circ f(x, y) \\ \circ \mathrm{transport}_{z:\mathbb{Z}.x \cdot z =_\mathbb{Z} x \cdot y}(y + 0, y, \mathrm{runitadd}_\mathbb{Z}(y)) \circ \mathrm{transport}_{z:\mathbb{Z}.x \cdot (y + 0) =_\mathbb{Z} z}(x \cdot y + 0, x \cdot y, \mathrm{runitadd}_\mathbb{Z}(x \cdot y)) \\ \circ \mathrm{transport}_{z:\mathbb{Z}.x \cdot (y + 0) =_\mathbb{Z} x \cdot y + z}(x \cdot 0, 0, \mathrm{rabsorp}_\mathbb{Z}(x)):(x \cdot (y + 0) =_\mathbb{Z} x \cdot y + x \cdot 0) \simeq (x \cdot (s(y) = 0) =_\mathbb{Z} x \cdot s(y) + x \cdot 0) \end{array}$$

Finally, we need to show that for all $y:\mathbb{Z}$ and $z:\mathbb{Z}$ there is an equivalence of types

$$(x \cdot (y + z) =_\mathbb{Z} x \cdot y + x \cdot z) \simeq (x \cdot (s(y) + s(z)) =_\mathbb{Z} x \cdot s(y) + x \cdot s(z))$$

…

Definition

The integer number one $1:\mathbb{Z}$ is defined as

$$1 \equiv s(0):\mathbb{Z}$$

Theorem

The integers type is a unital magma with respect to the one integer $1:\mathbb{Z}$ and multiplication $x:\mathbb{Z}, y:\mathbb{Z} \vdash x \cdot y:\mathbb{Z}$ both defined above.

Proof

We begin with the right unital laws, that $x \cdot s(0) =_\mathbb{Z} x$. By the computation rules for the integers type, we have

$$\beta_\mathbb{Z}^{\cdot, 0, s}(0):0 \cdot s(0) =_{\mathbb{Z}} 0 \cdot 0$$

Concatenating with $\beta_\mathbb{Z}^{\cdot, 0, 0}$ results in the required identification

$$\beta_\mathbb{Z}^{\cdot, 0, s}(0) \bullet \beta_\mathbb{Z}^{\cdot, 0, 0}:0 \cdot s(0) =_{\mathbb{Z}} 0$$

Then we need to show that for all $x:\mathbb{Z}$ we have an equivalence

$$(x \cdot s(0) =_{\mathbb{Z}} x) \simeq (s(x) \cdot s(0) =_{\mathbb{Z}} s(x))$$

We have the family of identifications

$$x:\mathbb{Z} \vdash \beta_\mathbb{Z}^{\cdot, s, s}(x, 0):s(x) \cdot s(0) =_{\mathbb{Z}} x \cdot 0 + s(x + 0)$$

Since multiplication is an absorption magma, we have identifications

$$\mathrm{rabsorp}_\mathbb{Z}(x):x \cdot 0 =_\mathbb{Z} 0$$

so application of the function $\lambda z:\mathbb{Z}.z + s(x + 0)$ to the above identification results in the identification

$$\mathrm{ap}_{\lambda z:\mathbb{Z}.z + s(x + 0)}(x \cdot 0, 0, \mathrm{rabsorp}_\mathbb{Z}(x)):x \cdot 0 + s(x + 0) =_{\mathbb{Z}} 0 + s(x + 0)$$

The left unit law for addition results in

$$\mathrm{lunitadd}_\mathbb{Z}(s(x + 0)):0 + s(x + 0) =_{\mathbb{Z}} s(x + 0)$$

and application of the successor equivalence to the right unit law results in

$$\mathrm{ap}_s(x + 0, x, \mathrm{runitadd}_\mathbb{Z}(x)):s(x + 0) =_{\mathbb{Z}} s(x)$$

Concatenating all the identifications leads to the identification

$$\beta_\mathbb{Z}^{\cdot, s, s}(x, 0) \bullet \mathrm{ap}_{\lambda z:\mathbb{Z}.z + s(x + 0)}(x \cdot 0, 0, \mathrm{rabsorp}_\mathbb{Z}(x)) \bullet \mathrm{lunitadd}_\mathbb{Z}(s(x + 0)) \bullet \mathrm{ap}_s(x + 0, x, \mathrm{runitadd}_\mathbb{Z}(x)):s(x) \cdot s(0) =_{\mathbb{Z}} s(x)$$

Similarly, by substituting $s^{-1}(x)$ in for $x$ in the above expression, we have

$$\beta_\mathbb{Z}^{\cdot, s, s}(s^{-1}(x), 0) \bullet \mathrm{ap}_{\lambda z:\mathbb{Z}.z + s(s^{-1}(x) + 0)}(s^{-1}(x) \cdot 0, 0, \mathrm{rabsorp}_\mathbb{Z}(s^{-1}(x))) \bullet \mathrm{lunitadd}_\mathbb{Z}(s(s^{-1}(x) + 0)) \bullet \mathrm{ap}_s(s^{-1}(x) + 0, s^{-1}(x), \mathrm{runitadd}_\mathbb{Z}(s^{-1}(x))):s(s^{-1}(x)) \cdot s(0) =_{\mathbb{Z}} s(s^{-1}(x))$$

In addition, we have the right inverse homotopy

$$\mathrm{rinv}_s:\prod_{x:\mathbb{Z}} s(s^{-1}(x)) =_\mathbb{Z} x$$

so by transport across the identity $\mathrm{rinv}_s(x)$ for the type family $z \cdot s(0) =_\mathbb{Z} x$, we also have the equivalence

$$\mathrm{transport}_{z:\mathbb{Z}.z \cdot s(0) =_\mathbb{Z} x}(s(s^{-1}(x)), x, \mathrm{rinv}_s(x)):(s(s^{-1}(x)) \cdot s(0) =_{\mathbb{Z}} x) \simeq (x \cdot s(0) =_{\mathbb{Z}} x)$$

Thus, we have the identification

$$\begin{array}{c} \mathrm{transport}_{z:\mathbb{Z}.z \cdot s(0) =_\mathbb{Z} x}(s(s^{-1}(x)), x, \mathrm{rinv}_s(x))(\beta_\mathbb{Z}^{\cdot, s, s}(s^{-1}(x), 0) \bullet \mathrm{ap}_{\lambda z:\mathbb{Z}.z + s(s^{-1}(x) + 0)}(s^{-1}(x) \cdot 0, 0, \mathrm{rabsorp}_\mathbb{Z}(s^{-1}(x))) \\ \bullet \mathrm{lunitadd}_\mathbb{Z}(s(s^{-1}(x) + 0)) \bullet \mathrm{ap}_s(s^{-1}(x) + 0, s^{-1}(x), \mathrm{runitadd}_\mathbb{Z}(s^{-1}(x))) \bullet \mathrm{rinv}_s(x)):x \cdot s(0) =_{\mathbb{Z}} x \end{array}$$

Since $\mathbb{Z}$ is a set, the identity types $x \cdot s(0) =_{\mathbb{Z}} x$ and $s(x) \cdot s(0) =_{\mathbb{Z}} s(x)$ are both propositions, and since they have identifications, both types are contractible types. All contractible types are equivalent to each other; thus there is an equivalence

$$f(x):(x \cdot s(0) =_{\mathbb{Z}} x) \simeq (s(x) \cdot s(0) =_{\mathbb{Z}} s(x))$$

Then, by induction on the integers, there is the homotopy

$$\mathrm{runitmul}_\mathbb{Z}:\mathrm{ind}_{\mathbb{Z}}^{x \cdot s(0) =_{\mathbb{Z}} x}(\beta_\mathbb{Z}^{\cdot, 0, s}(0) \bullet \beta_\mathbb{Z}^{\cdot, 0, 0}, \lambda x:\mathbb{Z}.f(x)):\prod_{x:\mathbb{Z}} x \cdot s(0) =_{\mathbb{Z}} x$$

Next, we derive the left unital laws, that $s(0) \cdot x =_\mathbb{Z} x$. By the computation rules for the integers type, we have

$$\beta_\mathbb{Z}^{\cdot, s, 0}(0):s(0) \cdot 0 =_{\mathbb{Z}} 0 \cdot 0$$

Concatenating with $\beta_\mathbb{Z}^{\cdot, 0, 0}$ results in the required identification

$$\beta_\mathbb{Z}^{\cdot, s, 0}(0) \bullet \beta_\mathbb{Z}^{\cdot, 0, 0}:s(0) \cdot 0 =_{\mathbb{Z}} 0$$

Then we need to show that for all $x:\mathbb{Z}$ we have an equivalence

$$(s(0) \cdot x =_{\mathbb{Z}} x) \simeq (s(0) \cdot s(x) =_{\mathbb{Z}} s(x))$$

We have the family of identifications

$$x:\mathbb{Z} \vdash \beta_\mathbb{Z}^{\cdot, s, s}(0, x):s(0) \cdot s(x) =_{\mathbb{Z}} 0 \cdot x + s(0 + x)$$

Since multiplication is an absorption magma, we have identifications

$$\mathrm{labsorp}_\mathbb{Z}(x):0 \cdot x =_\mathbb{Z} 0$$

so application of the function $\lambda z:\mathbb{Z}.z + s(0 + x)$ to the above identification results in the identification

$$\mathrm{ap}_{\lambda z:\mathbb{Z}.z + s(0 + x)}(0 \cdot x, 0, \mathrm{labsorp}_\mathbb{Z}(x)):0 \cdot x + s(0 + x) =_{\mathbb{Z}} 0 + s(0 + x)$$

The left unit law for addition results in

$$\mathrm{lunitadd}_\mathbb{Z}(s(0 + x)):0 + s(0 + x) =_{\mathbb{Z}} s(0 + x)$$

and application of the successor equivalence to the left unit law results in

$$\mathrm{ap}_s(0 + x, x, \mathrm{runitadd}_\mathbb{Z}(x)):s(0 + x) =_{\mathbb{Z}} s(x)$$

Concatenating all the identifications leads to the identification

$$\beta_\mathbb{Z}^{\cdot, s, s}(0, x) \bullet \mathrm{ap}_{\lambda z:\mathbb{Z}.z + s(0 + x)}(0 \cdot x, 0, \mathrm{labsorp}_\mathbb{Z}(x)) \bullet \mathrm{lunitadd}_\mathbb{Z}(s(0 + x)) \bullet \mathrm{ap}_s(0 + x, x, \mathrm{lunitadd}_\mathbb{Z}(x)):s(0) \cdot s(x) =_{\mathbb{Z}} s(x)$$

Similarly, by substituting $s^{-1}(x)$ in for $x$ in the above expression, we have

$$\beta_\mathbb{Z}^{\cdot, s, s}(0, s^{-1}(x)) \bullet \mathrm{ap}_{\lambda z:\mathbb{Z}.z + s(0 + s^{-1}(x))}(0 \cdot s^{-1}(x), 0, \mathrm{labsorp}_\mathbb{Z}(s^{-1}(x))) \bullet \mathrm{lunitadd}_\mathbb{Z}(s(0 + s^{-1}(x))) \bullet \mathrm{ap}_s(0 + s^{-1}(x), s^{-1}(x), \mathrm{lunitadd}_\mathbb{Z}(s^{-1}(x))):s(0) \cdot s(s^{-1}(x)) =_{\mathbb{Z}} s(s^{-1}(x))$$

In addition, we have the right inverse homotopy

$$\mathrm{rinv}_s:\prod_{x:\mathbb{Z}} s(s^{-1}(x)) =_\mathbb{Z} x$$

so by transport across the identity $\mathrm{rinv}_s(x)$ for the type family $s(0) \cdot z =_\mathbb{Z} x$, we also have the equivalence

$$\mathrm{transport}_{z:\mathbb{Z}.s(0) \cdot z =_\mathbb{Z} x}(s(s^{-1}(x)), x, \mathrm{rinv}_s(x)):s(0) \cdot (s(s^{-1}(x)) =_{\mathbb{Z}} x) \simeq (s(0) \cdot x =_{\mathbb{Z}} x)$$

Thus, we have the identification

$$\begin{array}{c} \mathrm{transport}_{z:\mathbb{Z}.s(0) \cdot z =_\mathbb{Z} x}(s(s^{-1}(x)), x, \mathrm{rinv}_s(x)) (\beta_\mathbb{Z}^{\cdot, s, s}(0, s^{-1}(x)) \bullet \mathrm{ap}_{\lambda z:\mathbb{Z}.z + s(0 + s^{-1}(x))}(0 \cdot s^{-1}(x), 0, \mathrm{labsorp}_\mathbb{Z}(s^{-1}(x))) \\ \bullet \mathrm{lunitadd}_\mathbb{Z}(s(0 + s^{-1}(x))) \bullet \mathrm{ap}_s(0 + s^{-1}(x), s^{-1}(x), \mathrm{lunitadd}_\mathbb{Z}(s^{-1}(x))) \bullet \mathrm{rinv}_s(x)):s(0) \cdot x =_{\mathbb{Z}} x \end{array}$$

Since $\mathbb{Z}$ is a set, the identity types $s(0) \cdot x =_{\mathbb{Z}} x$ and $s(0) \cdot s(x) =_{\mathbb{Z}} s(x)$ are both propositions, and since they have identifications, both types are contractible types. All contractible types are equivalent to each other; thus there is an equivalence

$$g(x):(s(0) \cdot x =_{\mathbb{Z}} x) \simeq (s(0) \cdot s(x) =_{\mathbb{Z}} s(x))$$

Then, by induction on the integers, there is the homotopy

$$\mathrm{lunitmul}_\mathbb{Z}:\mathrm{ind}_{\mathbb{Z}}^{s(0) \cdot x =_{\mathbb{Z}} x}(\beta_\mathbb{Z}^{\cdot, s, 0}(0) \bullet \beta_\mathbb{Z}^{\cdot, 0, 0}, \lambda x:\mathbb{Z}.g(x)):\prod_{x:\mathbb{Z}} s(0) \cdot x =_{\mathbb{Z}} x$$

Thus, $\mathbb{Z}$ is a unital magma with respect to one $1 \equiv s(0):\mathbb{Z}$ and multiplication $x:\mathbb{Z}, y:\mathbb{Z} \vdash x \cdot y:\mathbb{Z}$.

Theorem

Multiplication on the integers is associative.

Proof

….

Theorem

Multiplication on the integers is commutative.

Proof

….

Corollary

The integers are a commutative ring.

Exponentiation on the integers

Definition

The binary operation exponentiation is defined by induction on the natural numbers

Introduction rules for exponentiation:

$$\frac{\Gamma \; \mathrm{ctx}}{\Gamma, n:\mathbb{N}, x:\mathbb{Z}, \vdash x^n:\mathbb{Z}}$$

Computation rules for exponentiation:

$$\frac{\Gamma \; \mathrm{ctx}}{\Gamma, x:\mathbb{Z}, \vdash \beta_\mathbb{Z}^{x^{(-)}, 0}(x):x^0 =_\mathbb{Z} 1}$$

$$\frac{\Gamma \; \mathrm{ctx}}{\Gamma, n:\mathbb{N}, x:\mathbb{Z}, \vdash \beta_\mathbb{Z}^{x^{(-)}, s}:x^{s(n)} =_\mathbb{Z} x^n \cdot x}$$

Definition

The inclusion of the natural numbers in the integers is inductively defined by induction on the natural numbers

Introduction rules for natural number inclusion:

$$\frac{\Gamma \; \mathrm{ctx}}{\Gamma, n:\mathbb{N} \vdash i(n):\mathbb{Z}}$$

Computation rules for natural number inclusion:

$$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \beta_\mathbb{Z}^{i, 0}:i(0) =_\mathbb{Z} 0}$$

$$\frac{\Gamma \; \mathrm{ctx}}{\Gamma, n:\mathbb{N} \vdash \beta_\mathbb{Z}^{i, s}(n):i(s(n)) =_\mathbb{Z} s(i(n))}$$

Decidability of equality

Perhaps it is time to prove that equality is decidable on the integers.

Definition

The observational equality relation is defined by double induction on the integers

Formation rules for observational equality:

$$\frac{\Gamma \; \mathrm{ctx}}{\Gamma, x:\mathbb{Z}, y:\mathbb{Z} \vdash \mathrm{Eq}_\mathbb{Z}(x, y) \; \mathrm{type}}$$

Definition rules for observational equality:

$$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \beta_\mathbb{Z}^{\mathrm{Eq}_\mathbb{Z}, 0, 0}:\mathrm{Eq}_\mathbb{Z}(0, 0) \simeq \mathbb{1}}$$

$$\frac{\Gamma \; \mathrm{ctx}}{\Gamma, x:\mathbb{Z} \vdash \beta_\mathbb{Z}^{\mathrm{Eq}_\mathbb{Z}, 0, s}:\mathrm{Eq}_\mathbb{Z}(0, s(x)) \simeq \mathrm{Eq}_\mathbb{Z}(s^{-1}(0), x)}$$

$$\frac{\Gamma \; \mathrm{ctx}}{\Gamma, x:\mathbb{Z} \vdash \beta_\mathbb{Z}^{\mathrm{Eq}_\mathbb{Z}, 0, s}:\mathrm{Eq}_\mathbb{Z}(s(x), 0) \simeq \mathrm{Eq}_\mathbb{Z}(x, s^{-1}(0))}$$

$$\frac{\Gamma \; \mathrm{ctx}}{\Gamma, x:\mathbb{Z}, y:\mathbb{Z} \vdash \beta_\mathbb{Z}^{\mathrm{Eq}_\mathbb{Z}, s, s}:\mathrm{Eq}_\mathbb{Z}(s(x), s(y)) \simeq \mathrm{Eq}_\mathbb{Z}(x, y)}$$

The following rules only hold if the universe has a univalent universe:

$$\frac{\Gamma \; \mathrm{ctx}}{\Gamma, N:\mathbb{N} \vdash \beta_\mathbb{Z}^{\mathrm{Eq}_\mathbb{Z}, s, 0}:\mathrm{Eq}_\mathbb{Z}(0, i(n) + 1) \simeq \mathbb{0}}$$

$$\frac{\Gamma \; \mathrm{ctx}}{\Gamma, N:\mathbb{N} \vdash \beta_\mathbb{Z}^{\mathrm{Eq}_\mathbb{Z}, 0, s}:\mathrm{Eq}_\mathbb{Z}(i(n) + 1, 0) \simeq \mathbb{0}}$$

Order structure on the integers

Given a type family $x:A \vdash B(x)$, we define the existential quantifier $\exists x:A.B(x)$ as the propositional truncation of the dependent sum type $\left[\sum_{x:A} B(x)\right]$. Given two types $A$ and $B$, we define the disjunction $A \vee B$ as the propositional truncation of the sum type $\left[A + B\right]$.

Definition

The predicate is less than, denoted as $x \lt y$, is defined as

$$x \lt y \coloneqq \exists n:\mathbb{N}.x + i(n) + 1 =_\mathbb{N} y$$

for $x:\mathbb{Z}$, $y:\mathbb{Z}$.

Definition

The predicate is greater than, denoted as $x \gt y$, is defined as

$$x \gt y \coloneqq \exists n:\mathbb{N}.x =_\mathbb{N} y + i(n) + 1$$

for $x:\mathbb{Z}$, $y:\mathbb{Z}$.

Definition

The predicate is apart from, denoted as $x # y$, is defined as

$$x # y \coloneqq (x \lt y) \vee (x \gt y)$$

for $x:\mathbb{Z}$, $y:\mathbb{Z}$.

Definition

The predicate is less than or equal to, denoted as $x \leq y$, is defined as

$$x \leq y \coloneqq \exists n:\mathbb{N}.x + i(n) =_\mathbb{N} y$$

for $x:\mathbb{Z}$, $y:\mathbb{Z}$.

Definition

The predicate is greater than or equal to, denoted as $x \geq y$, is defined as

$$x \geq y \coloneqq \exists n:\mathbb{N}.x =_\mathbb{N} y + i(n)$$

for $x:\mathbb{Z}$, $y:\mathbb{Z}$.

Definition

The predicate is positive, denoted as $\mathrm{isPositive}(x)$, is defined as

$$\mathrm{isPositive}(x) \coloneqq \exists n:\mathbb{N}.i(n) + 1 =_\mathbb{N} x$$

for $x:\mathbb{Z}$.

Definition

The predicate is negative, denoted as $\mathrm{isNegative}(x)$, is defined as

$$\mathrm{isNegative}(x) \coloneqq \exists n:\mathbb{N}.x + i(n) + 1 =_\mathbb{N} 0$$

for $x:\mathbb{Z}$.

Definition

The predicate is zero, denoted as $\mathrm{isZero}(x)$, is defined as

$$\mathrm{isZero}(x) \coloneqq x =_\mathbb{Z} 0$$

for $x:\mathbb{Z}$.

Definition

The predicate is non-positive, denoted as $\mathrm{isNonPositive}(x)$, is defined as

$$\mathrm{isNonPositive}(x) \coloneqq \exists n:\mathbb{N}.0 =_\mathbb{N} x + i(n)$$

for $x:\mathbb{Z}$.

Definition

The predicate is non-negative, denoted as $\mathrm{isNonNegative}(x)$, is defined as

$$\mathrm{isNonNegative}(x) \coloneqq \exists n:\mathbb{N}.x =_\mathbb{N} i(n)$$

for $x:\mathbb{Z}$.

Definition

The predicate is non-zero, denoted as $\mathrm{isNonZero}(x)$, is defined as

$$\mathrm{isNonZero}(x) \coloneqq \mathrm{isPositive}(x) \vee \mathrm{isNegative}(x)$$

for $x:\mathbb{Z}$.

Pseudolattice and metric structure on the integers

Definition

The ramp function $\mathrm{ramp}:\mathbb{Z} \to \mathbb{Z}$ is defined as

$$\mathrm{ramp}(i(n)) \coloneqq i(n)$$

$$\mathrm{ramp}(-(i(n) + 1)) \coloneqq 0$$

for $n:\mathbb{N}$.

Definition

The minimum $\min:\mathbb{Z} \times \mathbb{Z} \to \mathbb{Z}$ is defined as

$$\min(x,y) \coloneqq x - \mathrm{ramp}(x - y)$$

for $x:\mathbb{Z}$, $y:\mathbb{Z}$.

Definition

The maximum $\max:\mathbb{Z} \times \mathbb{Z} \to \mathbb{Z}$ is defined as

$$\max(x,y) \coloneqq x + \mathrm{ramp}(y - x)$$

for $x:\mathbb{Z}$, $y:\mathbb{Z}$.

Definition

The metric $\rho:\mathbb{Z} \times \mathbb{Z} \to \mathbb{Z}$ is defined as

$$\rho(x,y) \coloneqq \max(x,y) - \min(x,y)$$

for $x:\mathbb{Z}$, $y:\mathbb{Z}$.

Definition

The absolute value $\vert(-)\vert:\mathbb{Z} \to \mathbb{Z}$ is defined as

$$\vert x \vert \coloneqq \max(x, -x)$$

for $x:\mathbb{Z}$.

Division and remainder

Definition

Integer division $(-)\div(-):\mathbb{Z} \times \mathbb{Z}_{\neq 0} \to \mathbb{Z}$ is defined as

$$i(n) \div i(m) \coloneqq i(n \div m)$$

$$i(n) \div -i(m) \coloneqq -i(n \div m)$$

$$-i(n) \div i(m) \coloneqq -i(n \div m)$$

$$-i(n) \div -i(m) \coloneqq i(n \div m)$$

for $n:\mathbb{N}$, $m:\mathbb{N}_{\neq 0}$.

Categorical semantics

The categorical semantics of the integers type is the integers object.

See also

• integers object

• natural numbers type

• equivalence type

• line type

• free group type?

References

For definitions as a higher inductive type in homotopy type theory, see:

• Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)

• 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)

A few more definitions of the integers, as well as the statement of the dependent universal property of the integers, could be found in:

• Egbert Rijke, Introduction to Homotopy Type Theory, Cambridge Studies in Advanced Mathematics, Cambridge University Press (arXiv:2212.11082)

Some terms about specific kinds of H-spaces used to prove properties of the integers are defined in:

• Ulrik Buchholtz, J. Daniel Christensen, Jarl G. Taxerås Flaten, Egbert Rijke, Central H-spaces and banded types [arXiv:2301.02636]

A formalization in terms of homotopy type theory, using a unary notation, is in

• Mike Shulman, Integers.v

(A different common formalization of integers in type theory is in a binary notation, as in the Coq standard library. Binary notation is exponentially more efficient for performing computations, but the unary notation was convenient for calculating $\pi_1(S^1)$.)

That one can construct the natural numbers type from the integers type can be found in:

• Christian Sattler, Natural numbers from integers (pdf)