Showing changes from revision #10 to #11:
Added | Removed | Changed
An A abelian proposition group is a pointed type set$(A,0)$ (A, A 0) with a an binary identification operation$(p-)-(-):\mathrm{Aa}\times {=}_{A}\mathrm{Ab}\to A$ (-)-(-):A p:a \times =_A A b \to A called for all elementssubtraction$a:A$ such and that$b:A$.
for all $a \in A$, $a - a = 0$
for all $a \in A$, $0 - (0 - a) = a$
for all $a \in A$ and $b \in A$, $a - (0 - b) = b - (0 - a)$
for all $a \in A$, $b \in A$, and $c \in A$, $a - (b - c) = (a - (0 - c)) - b$
A set is a type $A$ such that for all elements $a:A$ and $b:A$, the identity type $a =_A b$ is a proposition.
A halving group is an abelian group G with a function $(-)/2:G \to G$ called halving or dividing by two such that for all $g \in G$, $g/2 = g - g/2$.
A pointed abelian group is a set $A$ with an element $1:A$ called one and a binary operation $(-)-(-):A \times A \to A$ called subtraction such that
An abelian group $R$ is a totally ordered abelian group if it comes with a function $\max:R \times R \to R$ such that
for all elements $a:A$, $a - a = 1 - 1$
for all elements $a:A$, $(1 - 1) - ((1 - 1) - a) = a$
for all elements $a:A$ and $b:A$, $a - ((1 - 1) - b) = b - ((1 - 1) - a)$
for all elements $a:A$, $b:A$, and $c:A$, $a - (b - c) = (a - ((1 - 1) - c)) - b$
for all elements $a:R$, $\max(a, a) = a$
for all elements $a:R$ and $b:R$, $\max(a, b) = \max(b, a)$
for all elements $a:R$, $b:R$, and $c:R$, $\max(a, \max(b, c)) = \max(\max(a, b), c)$
for all elements $a:R$ and $b:R$, $\max(a, b) = b$ implies that for all elements $c:R$, $\max(a - c, b - c) = b - c$
for all elements $a:R$ and $b:R$, $\max(a, b) = a$ or $\max(a, b) = b$
A pointed halving group is a pointed abelian group G with a function $(-)/2:G \to G$ called halving or dividing by two such that for all elements $g:G$, $g/2 = g - g/2$.
A pointed halving group $R$ is a totally ordered pointed halving group if it comes with a function $\max:R \times R \to R$ such that
for all elements $a:R$, $\max(a, a) = a$
for all elements $a:R$ and $b:R$, $\max(a, b) = \max(b, a)$
for all elements $a:R$, $b:R$, and $c:R$, $\max(a, \max(b, c)) = \max(\max(a, b), c)$
for all elements $a:R$ and $b:R$, $\max(a, b) = a$ or $\max(a, b) = b$
for all elements $a:R$ and $b:R$, $\max(a, b) = b$ implies that for all elements $c:R$, $\max(a - c, b - c) = b - c$
A totally ordered commutative pointed ring halving group$R$ is a strictly ordered pointed abelian group if it comes with an a element type family$1<:R$ 1:R \lt and a type family $\lt$ such that
… The initial strictly ordered pointed halving group is the dyadic rational numbers$\mathbb{D}$.
A strictly ordered pointed halving group $A$ is an Archimedean ordered pointed halving group if for all elements $a:A$ and $b:A$, if $a \lt b$, then there merely exists a dyadic rational number $d:\mathbb{D}$ such that $a \lt h(d)$ and $h(d) \lt b$.
Let $A$ be an Archimedean ordered pointed halving group and let
be the positive elements in $A$ .$A$ is sequentially Cauchy complete if every Cauchy sequence in $A$ converges:
A sequence in $A$ is a function $x:\mathbb{N} \to A$.
A sequence $x:\mathbb{N} \to A$ is a Cauchy sequence if for all positive elements $\epsilon:A_{+}$, there merely exists a natural number $N:\mathbb{N}$ such that for all natural numbers $i:\mathbb{N}$ and $j:\mathbb{N}$ such that $N \leq i$ and $N \leq j$, $\max(x_i - x_j, x_j - x_i) \lt \epsilon$.
An element $l:A$ is said to be a limit of the sequence $x:\mathbb{N} \to A$ if for all positive elements $\epsilon:A_{+}$, there merely exists a natural number $N:\mathbb{N}$ such that for all natural numbers $i:\mathbb{N}$ such that $N \leq i$, $\max(x_i - l, l - x_i) \lt \epsilon$
$A$ is sequentially Cauchy complete if every Cauchy sequence in $A$ merely has a limit.