#Contents# * table of contents {:toc} ## 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 $(-)/(-) : \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)$$ ## See also ## * [[higher inductive type]] * [[natural numbers]] * [[integers]] * [[rational root theorem]] ## References ## * Univalent Foundations Project, [[HoTT book|Homotopy Type Theory – Univalent Foundations of Mathematics]] (2013) category: not redirected to nlab yet