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

Showing changes from revision #20 to #21: Added | Removed | Changed

Contents

Idea

The rational numbers as familiar from school mathematics.

Definition

The type of rational numbers, denoted \mathbb{Q}, is 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{Q}} \prod_{b:\mathbb{Q}} isProp(a=b)

See also

References

Revision on June 16, 2022 at 17:10:39 by Anonymous?. See the history of this page for a list of all contributions to it.