Contents
Idea
The rational numbers as familiar from school mathematics.
Definition
The type of rational numbers, denoted , is defined as the higher inductive type generated by:
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 is defined as
Definition
The binary operation addition is defined as
for , , , , , , .
Theorem
For any and , there are identities .
Definition
The unary operation negation is defined as
for , , .
Definition
The binary operation subtraction is defined as
for , , , , , , .
Definition
The rational number one is defined as
Definition
The binary operation multiplication is defined as
for , , , , , .
Definition
The right -action exponentiation is defined as
for , , , , .
This makes the rational numbers into a commutative ring.
Sign
Positive sign
We define the dependent type is positive, denoted as , to be the following:
for , , dependent types , indexed by .
Negative sign
We define the dependent type is negative, denoted as , to be the following:
for , , dependent types , indexed by .
Zero sign
We define the dependent type is zero, denoted as , to be the following:
for , .
Non-positive sign
We define the dependent type is non-positive, denoted as , to be the following:
for , .
Non-negative sign
We define the dependent type is non-negative, denoted as , to be the following:
for , .
Non-zero sign
We define the dependent type is non-zero, denoted as , to be the following:
for , .
Order structure on the rational numbers
Less than
We define the dependent type is less than, denoted as , to be the following:
for , , , .
Greater than
We define the dependent type is greater than, denoted as , to be the following:
for , , , .
Apart from
We define the dependent type is apart from, denoted as , to be the following:
for , , , .
Less than or equal to
We define the dependent type is less than or equal to, denoted as , to be the following:
for , , , .
Greater than or equal to
We define the dependent type is greater than or equal to, denoted as , to be the following:
for , , , .
Pseudolattice structure on the rational numbers
Ramp
We define the ramp function to be the following:
for , , , , , .
Minimum
We define the minimum to be the following:
for , , , .
Maximum
We define the maximum to be the following:
for , , , .
Absolute value
We define the absolute value to be the following:
for , .
See also
References
HoTT book