Homotopy Type Theory rational numbers > history (Rev #4)

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 ()/():× #0(-)/(-) : \mathbb{Z} \times \mathbb{Z}_{#0} \rightarrow \mathbb{Q}, where
    #0 a:a#0\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: a: b: #0 c: d: #0(ai(d)=ci(b))(a/b=c/d)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: #0i: \mathbb{Z}_{#0} \to \mathbb{Z} is the inclusion of the nonzero integers in the integers.

  • A set-truncator
    τ 0: a: b:isProp(a=b)\tau_0: \prod_{a:\mathbb{Z}} \prod_{b:\mathbb{Z}} isProp(a=b)

Properties

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

See also

References

HoTT book

Revision on February 26, 2022 at 15:51:54 by Anonymous?. See the history of this page for a list of all contributions to it.