Homotopy Type Theory rational numbers > history (Rev #6, changes)

Showing changes from revision #5 to #6: Added | Removed | Changed

Idea

The rational numbers as familiar from school mathematics.

Definition

The type of rational numbers, denoted $\mathbb{Q}$, has several definitions as a higher inductive type.

Definition 1

The rational numbers are defined as the higher inductive type generated by:

• A function $(-)/(-) : \mathbb{Z} \times \mathbb{Z}_{#0} \rightarrow \mathbb{Q}$, where
  $$\mathbb{Z}_{#0} \coloneqq \sum_{a:\mathbb{Z}} a # 0$$

  and $#$ is the apartness relation on the integers.

• A dependent product of functions between identities representing that equivalent fractions are equal:
  $$equivfrac : \prod_{a:\mathbb{Z}} \prod_{b:\mathbb{Z}_{#0}} \prod_{c:\mathbb{Z}} \prod_{d:\mathbb{Z}_{#0}} (a \cdot i(d) = c \cdot i(b)) \to (a/b = c/d)$$

  where $i: \mathbb{Z}_{#0} \to \mathbb{Z}$ is the inclusion of the nonzero integers in the integers.

• A set-truncator
  $$\tau_0: \prod_{a:\mathbb{Q}} \prod_{b:\mathbb{Q}} isProp(a=b)$$

Properties

TODO: Show that the rational numbers are a an Heyting ordered Heyting field with decidable equality, decidable apartness, and decidable linear order, and that the rational numbers are initial in the category of Heyting ordered Heyting fields. The HoTT book unfortunately skips the proof entirely.

See also

• higher inductive type
• integers
• decimal numbers

References

HoTT book