# Homotopy Type Theory an axiomatization of the real numbers > history (Rev #10, changes)

Showing changes from revision #9 to #10: Added | Removed | Changed

## Definition

### Totally Abelian ordered abelian groups

An abelian group$R$abelian group is a totally pointed ordered set abelian group if it comes with a function \max:R (A, \times 0) R \to R with a binary operation $(-)-(-):A \times A \to A$ called subtraction such that

• for all elements a:R a \in A,  \max(a, a) = a - a = 0

• for all elements a:R a \in A , and b:R 0 - (0 - a) = a, $\max(a, b) = \max(b, a)$

• for all elements a:R a \in A , and b:R b \in A , and c:R a - (0 - b) = b - (0 - a), $\max(a, \max(b, c)) = \max(\max(a, b), c)$

• for all elements a:R a \in A , and b:R b \in A , and \max(a, c b) \in = A b , implies that for all elements c:R a - (b - c) = (a - (0 - c)) - b, $\max(a + c, b + c) = b + c$

• for all elements $a:R$ and $b:R$, $\max(a, b) = a$ or $\max(a, b) = b$

### Strictly Halving ordered pointed abelian groups

A totally ordered commutative ring$R$halving group is a an strictly ordered pointed abelian group if it comes with an element$1:R$G and with a type function family \lt (-)/2:G \to G such called thathalving or dividing by two such that for all $g \in G$, $g/2 = g - g/2$.

• for all elements $a:R$ and $b:R$, $a \lt b$ is a proposition
• for all elements $a:R$, $a \lt a$ is false
• for all elements $a:R$, $b:R$, and $c:R$, if $a \lt c$, then $a \lt b$ or $b \lt c$
• for all elements $a:R$ and $b:R$, if $a \lt b$ is false and $b \lt a$ is false, then $a = b$
• for all elements $a:R$ and $b:R$, if $a \lt b$, then $b \lt a$ is false.
• $0 \lt 1$
• for all elements $a:R$ and $b:R$, if $0 \lt a$ and $0 \lt b$, then $0 \lt a + b$

### Strictly ordered pointed $\mathbb{Q}$-vector space

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: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$

### Strictly ordered pointed halving groups

A totally ordered commutative ring $R$ is a strictly ordered pointed abelian group if it comes with an element $1:R$ and a type family $\lt$ such that

• for all elements $a:R$ and $b:R$, $a \lt b$ is a proposition
• for all elements $a:R$, $a \lt a$ is false
• for all elements $a:R$, $b:R$, and $c:R$, if $a \lt c$, then $a \lt b$ or $b \lt c$
• for all elements $a:R$ and $b:R$, if $a \lt b$ is false and $b \lt a$ is false, then $a = b$
• for all elements $a:R$ and $b:R$, if $a \lt b$, then $b \lt a$ is false.
• $0 \lt 1$
• for all elements $a:R$ and $b:R$, if $0 \lt a$ and $0 \lt b$, then $0 \lt a - (0 - b)$

### Archimedean ordered pointed halving groups$\mathbb{Q}$-vector space

A strictly ordered pointed halving group \mathbb{Q} A -vector space is an Archimedean ordered pointed halving group if for all elements A a:A is and an Archimedean ordered pointed \mathbb{Q} b:A -vector , space if for all elements a:A a \lt b , and then there merely exists a dyadic rational number b:A d:\mathbb{D} , if such that a \lt b h(d) , then and there merely exists a rational number q:\mathbb{Q} h(d) \lt b such that $a \lt h(q)$ and $h(q) \lt b$.

### Sequentially Cauchy complete Archimedean ordered pointed halving groups$\mathbb{Q}$-vector space

Let $A$ be an Archimedean ordered pointed halving group and let$\mathbb{Q}$-vector space and let

$A_{+} \coloneqq \sum_{a:A} 0 \lt a$

be the positive elements in $A$. $A$ is sequentially Cauchy complete if every Cauchy sequence in $A$ converges:

$isCauchy(x) \coloneqq \forall \epsilon \in A_{+}. \exists N \in I. \forall i \in I. \forall j \in I. (i \geq N) \wedge (j \geq N) \wedge (\vert x_i - x_j \vert \lt \epsilon)$
$isLimit(x, l) \coloneqq \forall \epsilon \in A_{+}. \exists N \in I. \forall i \in I. (i \geq N) \to (\vert x_i - l \vert \lt \epsilon)$
$\forall x: \mathbb{N} \to A. isCauchy(x) \wedge \exists l \in A. isLimit(x, l)$

Revision on June 17, 2022 at 19:34:22 by Anonymous?. See the history of this page for a list of all contributions to it.