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 $(-)/(-) : \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

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:

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:

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:

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:

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:

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:

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:

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:

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:

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:

for $a:\mathbb{Z}$, $b:\mathbb{Z}_{#0}$.

See also

• higher inductive type
• integers
• decimal numbers
• real numbers

References

HoTT book