Homotopy Type Theory rational numbers > history (Rev #10, changes)

Showing changes from revision #9 to #10: Added | ~~Removed~~ | ~~Chan~~ged

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

Definition

The rational number zero $0:\mathbb{Q}$ is defined as

0 \coloneqq 0/1

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}$ .

Theorem

For any $q:\mathbb{Q}$ and $r:\mathbb{Q}$ , there are identities $p: q + r = r + q$ .

Proof

TODO

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}$ .

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}$ .

Definition

The rational number one $1:\mathbb{Q}$ is defined as

1 \coloneqq 1/1

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}$ .

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~~

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}$ .

~~We define the dependent type is less than, denoted as $a/b \lt c/d$ , to be the following:~~

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}$ .

~~$a/b \lt c/d \coloneqq isPositive(c/d - a/b)$~~

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}$ .

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

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}$ .

~~Greater than~~

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}$ .

~~We define the dependent type is greater than, denoted as $a/b \gt c/d$ , to be the following:~~

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}$ .

~~$a/b \gt c/d \coloneqq isNegative(c/d - a/b)$~~

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}$ .

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

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}$ .

~~Apart from~~

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}$ .

~~We define the dependent type is apart from, denoted as $a/b # c/d$ , to be the following:~~

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}$ .

~~$a/b # c/d \coloneqq isNonZero(c/d - a/b)$~~

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}$ .

~~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

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}$ .

~~The minimum $min:\mathbb{Q} \times \mathbb{Q} \to \mathbb{Q}$ is defined as~~

Definition

~~$min(a/b,c/d) \coloneqq a/b - ramp(a/b - c/d)$~~

The minimum $min:\mathbb{Q} \times \mathbb{Q} \to \mathbb{Q}$ is defined as

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

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}$ .

~~The maximum $max:\mathbb{Q} \times \mathbb{Q} \to \mathbb{Q}$ is defined as~~

Definition

~~$max(a/b,c/d) \coloneqq a/b + ramp(c/d - a/b)$~~

The maximum $max:\mathbb{Q} \times \mathbb{Q} \to \mathbb{Q}$ is defined as

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

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}$ .

~~The absolute value $\vert(-)\vert:\mathbb{Q} \to \mathbb{Q}$ is defined as~~

Definition

~~$\vert a/b \vert \coloneqq max(a/b, -a/b)$~~

The absolute value $\vert(-)\vert:\mathbb{Q} \to \mathbb{Q}$ is defined as

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

\vert a/b \vert \coloneqq max(a/b, -a/b)

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

References

HoTT book

Revision on February 27, 2022 at 17:46:56 by Anonymous?. See the history of this page for a list of all contributions to it.

Homotopy Type Theory rational numbers > history (Rev #10, changes)

Contents

Idea

Definition

Properties

Commutative ring structure on the rational numbers

Definition

Definition

Theorem

Proof

Definition

Definition

Definition

Definition

Definition

Sign

Positive sign

Negative sign

Zero sign

Non-positive sign

Non-negative sign

Non-zero sign

Order structure on the rational numbers

Less than

Definition

Definition

Definition

Definition

Greater than

Definition

Definition

Definition

Definition

Apart from

Definition

Definition

Definition

Less than or equal to

Greater than or equal to

Pseudolattice structure on the rational numbers

Definition

Definition

Definition

Definition

See also

References