#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. ### Sign ### #### Positive sign #### We define the dependent type *is positive*, denoted as $isPositive(a/b)$, to be the following: $$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}$. #### Negative sign #### We define the dependent type *is negative*, denoted as $isNegative(a/b)$, to be the following: $$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}$. #### Zero sign #### We define the dependent type *is zero*, denoted as $isZero(a/b)$, to be the following: $$isZero(a/b) \coloneqq a = 0$$ for $a:\mathbb{Z}$, $b:\mathbb{Z}_{#0}$. #### Non-positive sign #### We define the dependent type *is non-positive*, denoted as $isNonPositive(a/b)$, to be the following: $$isNonPositive(a/b) \coloneqq isPositive(a/b) \to \emptyset$$ for $a:\mathbb{Z}$, $b:\mathbb{Z}_{#0}$. #### Non-negative sign #### We define the dependent type *is non-negative*, denoted as $isNonNegative(a/b)$, to be the following: $$isNonNegative(a/b) \coloneqq isNegative(a/b) \to \emptyset$$ for $a:\mathbb{Z}$, $b:\mathbb{Z}_{#0}$. #### Non-zero sign #### We define the dependent type *is non-zero*, denoted as $isNonZero(a/b)$, to be the following: $$isNonNegative(a/b) \coloneqq \Vert isPositive(a/b) + isNegative(a/b) \Vert$$ for $a:\mathbb{Z}$, $b:\mathbb{Z}_{#0}$. ### Order structure on the rational numbers ### #### Less than #### We define the dependent type *is less than*, denoted as $a/b \lt c/d$, to be the following: $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}$. #### Greater than #### We define the dependent type *is greater than*, denoted as $a/b \gt c/d$, to be the following: $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}$. #### Apart from #### We define the dependent type *is apart from*, denoted as $a/b # c/d$, to be the following: $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}$. #### Less than or equal to #### We define the dependent type *is less than or equal to*, denoted as $a/b \leq c/d$, to be the following: $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}$. #### Greater than or equal to #### We define the dependent type *is greater than or equal to*, denoted as $a/b \geq c/d$, to be the following: $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 ### #### Ramp #### We define the *ramp function* $ramp:\mathbb{Q} \to \mathbb{Q}$ to be the following: $$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}$. #### Minimum #### We define the *minimum* $min:\mathbb{Q} \times \mathbb{Q} \to \mathbb{Q}$ to be the following: $$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}$. #### Maximum #### We define the *maximum* $max:\mathbb{Q} \times \mathbb{Q} \to \mathbb{Q}$ to be the following: $$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}$. #### Absolute value #### We define the *absolute value* $\vert(-)\vert:\mathbb{Q} \to \mathbb{Q}$ to be the following: $$\vert a/b \vert \coloneqq max(a/b, -a/b)$$ for $a:\mathbb{Z}$, $b:\mathbb{Z}_{#0}$. ## See also ## * [[higher inductive type]] * [[integers]] * [[decimal numbers]] * [[real numbers]] ## References ## [[HoTT book]]