Homotopy Type Theory integers > history (Rev #1)

Idea

The integers as familiar from school mathematics.

Definition

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}$.
• A term representing that positive and negative zero are equal: $\nu_0: inj(0, 0) = inj(1, 0)$.
• A set-truncator
  $$\tau_0: \prod_{a:\mathbb{Z}} \prod_{b:\mathbb{Z}} isProp(a=b)$$

Definition 2

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

• A function $inj : \mathbb{N} \times \mathbb{N} \rightarrow \mathbb{Z}$.
• A term 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