Showing changes from revision #12 to #13:
Added | Removed | Changed
Contents
< real number
Definition
Propositions
A proposition is a type with an identification for all elements and .
Sets
A set is a type such that for all elements and , the identity type is a proposition.
Pointed abelian groups
A pointed abelian group is a set with an element called one and a binary operation called subtraction such that
-
for all elements ,
-
for all elements ,
-
for all elements and ,
-
for all elements , , and ,
Pointed halving groups
A pointed halving group is a pointed abelian group G with a function called halving or dividing by two such that for all elements , .
Totally ordered pointed halving groups
A pointed halving group is a totally ordered pointed halving group if it comes with a function such that
-
for all elements ,
-
for all elements and ,
-
for all elements , , and ,
-
for all elements and , or
-
for all elements and , implies that for all elements ,
Strictly ordered pointed halving groups
A totally ordered pointed halving group is a strictly ordered pointed abelian group if it comes with a type family such that
- for all elements and , is a proposition
- for all elements , is false
- for all elements , , and , if , then or
- for all elements and , if is false and is false, then
- for all elements and , if , then is false.
- for all elements and , if and , then
The homotopy initial strictly ordered pointed halving group is the dyadic rational numbers .
Archimedean ordered pointed halving groups
A strictly ordered pointed halving group is an Archimedean ordered pointed halving group if for all elements and , if , then there merely exists a dyadic rational number such that and .
Sequentially Cauchy complete Archimedean ordered pointed halving groups
Let be an Archimedean ordered pointed halving group and let
be the positive elements in .
A sequence in is a function .
A sequence is a Cauchy sequence if for all positive elements , there merely exists a natural number such that for all natural numbers and such that and , .
An element is said to be a limit of the sequence if for all positive elements , there merely exists a natural number such that for all natural numbers such that ,
is sequentially Cauchy complete if every Cauchy sequence in merely has a limit.