#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)$$ ## Properties ## TODO: Show that the rational numbers are an ordered Heyting field with decidable equality, decidable apartness, and decidable linear order, and that the rational numbers are initial in the category of ordered Heyting fields. The HoTT book unfortunately skips the proof entirely. ### Commutative ring structure on the rational numbers ### +--{: .num_defn} ###### Definition The rational number **zero** $0:\mathbb{Q}$ is defined as $$0 \coloneqq 0/1$$ =-- +--{: .num_defn} ###### Definition The binary operation **addition** $(-)+(-):\mathbb{Q} \times \mathbb{Q} \to \mathbb{Q}$ is defined as $$a/b + c/d \coloneqq (a \cdot i(d) + c \cdot i(b))/(b \cdot d)$$ for $a:\mathbb{Z}$, $b:\mathbb{Z}_{#0}$, $c:\mathbb{Z}$, $d:\mathbb{Z}_{#0}$, $(-)+(-):\mathbb{Z} \times \mathbb{Z} \to \mathbb{Z}$, $(-)\cdot(-):\mathbb{Z} \times \mathbb{Z} \to \mathbb{Z}$, $i: \mathbb{Z}_{#0} \to \mathbb{Z}$. =-- +--{: .num_theorem} ###### Theorem For any $q:\mathbb{Q}$ and $r:\mathbb{Q}$, there are identities $p: q + r = r + q$. =-- +--{: .proof} ###### Proof TODO =-- +--{: .num_defn} ###### Definition The unary operation **negation** $-(-):\mathbb{Q} \to \mathbb{Q}$ is defined as $$-(a/b) \coloneqq (-a)/b$$ for $a:\mathbb{Z}$, $b:\mathbb{Z}_{#0}$, $-(-):\mathbb{Z} \to \mathbb{Z}$. =-- +--{: .num_defn} ###### Definition The binary operation **subtraction** $(-)-(-):\mathbb{Q} \times \mathbb{Q} \to \mathbb{Q}$ is defined as $$a/b - c/d \coloneqq (a \cdot i(d) - c \cdot i(b))/(b \cdot d)$$ for $a:\mathbb{Z}$, $b:\mathbb{Z}_{#0}$, $c:\mathbb{Z}$, $d:\mathbb{Z}_{#0}$, $(-)-(-):\mathbb{Z} \times \mathbb{Z} \to \mathbb{Z}$, $(-)\cdot(-):\mathbb{Z} \times \mathbb{Z} \to \mathbb{Z}$, $i: \mathbb{Z}_{#0} \to \mathbb{Z}$. =-- +--{: .num_defn} ###### Definition The rational number **one** $1:\mathbb{Q}$ is defined as $$1 \coloneqq 1/1$$ =-- +--{: .num_defn} ###### Definition The binary operation **multiplication** $(-)\cdot(-):\mathbb{Q} \times \mathbb{Q} \to \mathbb{Q}$ is defined as $$a/b \cdot c/d \coloneqq (a \cdot c)/(b \cdot d)$$ for $a:\mathbb{Z}$, $b:\mathbb{Z}_{#0}$, $c:\mathbb{Z}$, $d:\mathbb{Z}_{#0}$, $(-)\cdot(-):\mathbb{Z} \times \mathbb{Z} \to \mathbb{Z}$, $i: \mathbb{Z}_{#0} \to \mathbb{Z}$. =-- +--{: .num_defn} ###### Definition The right $\mathbb{N}$-action **exponentiation** $(-)^{(-)}:\mathbb{Q} \times \mathbb{N} \to \mathbb{Q}$ is defined as $$(a/b)^n \coloneqq (a^n)/(b^n)$$ for $a:\mathbb{Z}$, $b:\mathbb{Z}_{#0}$, $n:\mathbb{N}$, $(-)^{(-)}:\mathbb{Z} \times \mathbb{N} \to \mathbb{Z}$, $(-)^{(-)}:\mathbb{Z}_{#0} \times \mathbb{N} \to \mathbb{Z}_{#0}$. =-- This makes the rational numbers into a commutative ring. ### Order structure on the rational numbers ### +--{: .num_defn} ###### Definition The dependent type *is positive*, denoted as $isPositive(a/b)$, is defined as $$isPositive(a/b) \coloneqq \Vert (a \gt 0) \times (i(b) \gt 0) + (a \lt 0) \times (i(b) \lt 0) \Vert$$ for $a:\mathbb{Z}$, $b:\mathbb{Z}_{#0}$, dependent types $m\lt n$, $m\gt n$ indexed by $m, n:\mathbb{Z}$. =-- +--{: .num_defn} ###### Definition The dependent type *is negative*, denoted as $isNegative(a/b)$, is defined as $$isNegative(a/b) \coloneqq \Vert (a \gt 0) \times (i(b) \lt 0) + (a \lt 0) \times (i(b) \gt 0) \Vert$$ for $a:\mathbb{Z}$, $b:\mathbb{Z}_{#0}$, dependent types $m\lt n$, $m\gt n$ indexed by $m, n:\mathbb{Z}$. =-- +--{: .num_defn} ###### Definition The dependent type *is zero*, denoted as $isZero(a/b)$, is defined as $$isZero(a/b) \coloneqq a = 0$$ for $a:\mathbb{Z}$, $b:\mathbb{Z}_{#0}$. =-- +--{: .num_defn} ###### Definition The dependent type *is non-positive*, denoted as $isNonPositive(a/b)$ is defined as $$isNonPositive(a/b) \coloneqq isPositive(a/b) \to \emptyset$$ for $a:\mathbb{Z}$, $b:\mathbb{Z}_{#0}$. =-- +--{: .num_defn} ###### Definition The dependent type *is non-negative*, denoted as $isNonNegative(a/b)$, is defined as $$isNonNegative(a/b) \coloneqq isNegative(a/b) \to \emptyset$$ for $a:\mathbb{Z}$, $b:\mathbb{Z}_{#0}$. =-- +--{: .num_defn} ###### Definition The dependent type *is non-zero*, denoted as $isNonZero(a/b)$, is defined as $$isNonZero(a/b) \coloneqq \Vert isPositive(a/b) + isNegative(a/b) \Vert$$ for $a:\mathbb{Z}$, $b:\mathbb{Z}_{#0}$. =-- +--{: .num_defn} ###### Definition The dependent type *is less than*, denoted as $a/b \lt c/d$, is defined as $a/b \lt c/d \coloneqq isPositive(c/d - a/b)$ for $a:\mathbb{Z}$, $b:\mathbb{Z}_{#0}$, $c:\mathbb{Z}$, $d:\mathbb{Z}_{#0}$. =-- +--{: .num_defn} ###### Definition The dependent type *is greater than*, denoted as $a/b \gt c/d$, is defined as $a/b \gt c/d \coloneqq isNegative(c/d - a/b)$ for $a:\mathbb{Z}$, $b:\mathbb{Z}_{#0}$, $c:\mathbb{Z}$, $d:\mathbb{Z}_{#0}$. =-- +--{: .num_defn} ###### Definition The dependent type *is apart from*, denoted as $a/b # c/d$, is defined as $a/b # c/d \coloneqq isNonZero(c/d - a/b)$ for $a:\mathbb{Z}$, $b:\mathbb{Z}_{#0}$, $c:\mathbb{Z}$, $d:\mathbb{Z}_{#0}$. =-- +--{: .num_defn} ###### Definition The dependent type *is less than or equal to*, denoted as $a/b \leq c/d$, is defined as $a/b \leq c/d \coloneqq isNonNegative(c/d - a/b)$ for $a:\mathbb{Z}$, $b:\mathbb{Z}_{#0}$, $c:\mathbb{Z}$, $d:\mathbb{Z}_{#0}$. =-- +--{: .num_defn} ###### Definition The dependent type *is greater than or equal to*, denoted as $a/b \geq c/d$, is defined as $a/b \geq c/d \coloneqq isNonPositive(c/d - a/b)$ for $a:\mathbb{Z}$, $b:\mathbb{Z}_{#0}$, $c:\mathbb{Z}$, $d:\mathbb{Z}_{#0}$. =-- ### Pseudolattice structure on the rational numbers ### +--{: .num_defn} ###### Definition The **ramp function** $ramp:\mathbb{Q} \to \mathbb{Q}$ is defined as $$ramp(a/b) \coloneqq (ramp(a) \cdot ramp(i(b)) + ramp(-a) \cdot ramp(i(-b)))/(b \cdot b)$$ for $a:\mathbb{Z}$, $b:\mathbb{Z}_{#0}$, $ramp:\mathbb{Z} \to \mathbb{Z}$, $(-)+(-):\mathbb{Z} \times \mathbb{Z} \to \mathbb{Z}$, $(-)\cdot(-):\mathbb{Z} \times \mathbb{Z} \to \mathbb{Z}$, $i: \mathbb{Z}_{#0} \to \mathbb{Z}$. =-- +--{: .num_defn} ###### Definition The **minimum** $min:\mathbb{Q} \times \mathbb{Q} \to \mathbb{Q}$ is defined as $$min(a/b,c/d) \coloneqq a/b - ramp(a/b - c/d)$$ for $a:\mathbb{Z}$, $b:\mathbb{Z}_{#0}$, $c:\mathbb{Z}$, $d:\mathbb{Z}_{#0}$. =-- +--{: .num_defn} ###### Definition The **maximum** $max:\mathbb{Q} \times \mathbb{Q} \to \mathbb{Q}$ is defined as $$max(a/b,c/d) \coloneqq a/b + ramp(c/d - a/b)$$ for $a:\mathbb{Z}$, $b:\mathbb{Z}_{#0}$, $c:\mathbb{Z}$, $d:\mathbb{Z}_{#0}$. =-- +--{: .num_defn} ###### Definition The **absolute value** $\vert(-)\vert:\mathbb{Q} \to \mathbb{Q}$ is defined as $$\vert a/b \vert \coloneqq max(a/b, -a/b)$$ for $a:\mathbb{Z}$, $b:\mathbb{Z}_{#0}$. =-- ## See also ## * [[higher inductive type]] * [[natural numbers]] * [[integers]] * [[decimal numbers]] * [[real numbers]] ## References ## * Univalent Foundations Project, [[HoTT book|Homotopy Type Theory – Univalent Foundations of Mathematics]] (2013)