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.

Abelian group structure on the integers

Definition

The binary operation addition is defined by double induction on the integers type

Introduction rules for addition:

$$\frac{\Gamma \; \mathrm{ctx}}{\Gamma, x:\mathbb{Z}, y:\mathbb{Z} \vdash x + y:\mathbb{Z}}$$

Computation rules for addition:

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

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

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

$$\frac{\Gamma \; \mathrm{ctx}}{\Gamma, x:\mathbb{Z}, y:\mathbb{Z} \vdash \beta_\mathbb{Z}^{+, s, s}(x, y):s(x) + s(y) =_\mathbb{Z} s(s(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

$$\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$$

$$\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 a non-coherent A3-space, an associative non-coherent H-space.

Proof

…

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

…

Theorem

The integers type $\mathbb{Z}$ is a monoid, a 0-truncated non-coherent A3-space.

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 a non-coherent A3-space, this implies that $\mathbb{Z}$ is a monoid.

Theorem

The integers type is a group, a monoid such that given an integer $x:\mathbb{Z}$, left addition and right addition by $x$ is each an equivalence of types.

Proof

…

Theorem

The integers type is an abelian group.

Proof

…

Definition

The unary operation negation is defined by induction on the integers type

Introduction rules for negation:

$$\frac{\Gamma \; \mathrm{ctx}}{\Gamma, x:\mathbb{Z} \vdash -x:\mathbb{Z}}$$

Computation rules for negation:

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

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

where $s^{-1}:\mathbb{Z} \simeq \mathbb{Z}$ is the inverse equivalence of $s:\mathbb{Z} \simeq \mathbb{Z}$.

Definition

The binary operation subtraction is defined as

$$x - y \coloneqq x + (- y)$$

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

Commutative ring structure on the integers

Definition

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

$$1 \coloneqq s(0)$$

Definition

The binary operation multiplication is defined by double induction on the integers

Introduction rules for multiplication:

$$\frac{\Gamma \; \mathrm{ctx}}{\Gamma, x:\mathbb{Z}, y:\mathbb{Z} \vdash x \cdot y:\mathbb{Z}}$$

Computation rules for multiplication:

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

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

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

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

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}$.

See also

• natural numbers type

• equivalence 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)$.)