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

Showing changes from revision #1 to #2: 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}_+ \rightarrow \mathbb{Q}, where
    + a:0<a\mathbb{Z}_+ \coloneqq \sum_{a:\mathbb{Z}} 0 \lt a
  • A term representing that equivalent fractions are equal:
    equivfrac: a: b: + c: d: +(ai(d)=ci(b))(a/b=c/d)equivfrac : \prod_{a:\mathbb{Z}} \prod_{b:\mathbb{Z}_+} \prod_{c:\mathbb{Z}} \prod_{d:\mathbb{Z}_+} (a \cdot i(d) = c \cdot i(b)) \to (a/b = c/d)

    where i: +i: \mathbb{Z}_+ \to \mathbb{Z} is the inclusion of the positive integers in the integers.

  • A set-truncator
    τ 0: a: b:isProp(a=b) \tau_0: \prod_{a:\mathbb{Q}} \prod_{a:\mathbb{Z}} \prod_{b:\mathbb{Q}} \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 13:49:06 by Anonymous?. See the history of this page for a list of all contributions to it.