Showing changes from revision #6 to #7:
Added | Removed | Changed
Contents
Idea
The rational numbers as familiar from school mathematics.
Definition
The type of rational numbers, denoted , has is several defined definitions as a thehigher inductive type . generated by:
Definition 1
The rational numbers are defined as the higher inductive type generated by:
Mathematical structures on the rational numbers
Ring structure on the rational numbers
Zero
We define zero to be the following:
Addition
We define addition to be the following:
for , , , , , , .
Negation
We define negation to be the following:
for , , .
Subtraction
We define subtraction to be the following:
for , , , , , , .
One
We define one to be the following:
Multiplication
We define multiplication to be the following:
for , , , , , .
Exponentiation
We define exponentiation to be the following:
for , , , , .
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 , .
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.
See also
References
HoTT book