## 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 $$\mathbb{Z}_+ \coloneqq \sum_{a:\mathbb{Z}} 0 \lt a$$ * A term representing that equivalent fractions are equal: $$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: \mathbb{Z}_+ \to \mathbb{Z}$ is the inclusion of the positive integers in the integers. * A set-truncator $$\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 ## * [[higher inductive type]] * [[integers]] * [[decimal numbers]] ## References ## [[HoTT book]]