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

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

## Definition

### Totally ordered commutative abelian rings groups

A An commutative abelian ring group$R$ is a totally ordered commutative abelian ring 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, 0) b) = a and or \max(b, \max(a, 0) b) = b implies $\max(a \cdot b, 0) = a \cdot b$

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

### Totally Strictly ordered commutative pointed abelian groups$\mathbb{Q}$-algebras

Given A totally ordered commutative rings ring$R$ and is a strictly ordered pointed abelian group if it comes with an element S 1:R , and a commutative type ring family homomorphism h:R \lt \to S is such monotonic that if for all$a:R$ and $b:R$, $\max(h(a), h(b)) = h(\max(a, b))$.

Every totally ordered commutative ring $R$ has a monotonic commutative ring homomorphism $h:\mathbb{Z} \to R$ from the integers to $R$, and there is an monotonic injection $i:\mathbb{Z}_+ \to \mathbb{Z}$ from the positive integers to the integers.

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

A totally ordered commutative ring $R$ is a totally ordered commutative $\mathbb{Q}$-algebra if there is a function $j:\mathbb{Z}_+ \to R$ such that for all positive integers $a:\mathbb{Z}_+$, $h(i(a)) \cdot j(a) = 1$.

### Strictly ordered integral ring

A totally ordered commutative ring $R$ is a strictly ordered integral ring if it comes with a type family $\lt$ such that

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

• 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$
• for all elements $a:R$ and $b:R$, if $0 \lt a$ and $0 \lt b$, then $0 \lt a \cdot b$
• for all elements $a:R$ and $b:R$, if $0 \lt \max(a, -a)$ and $0 \lt \max(b, -b)$, then $0 \lt \max(a \cdot b, -a \cdot b)$

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

### Strictly Sequentially Cauchy complete Archimedean ordered integral pointed$\mathbb{Q}$ -algebras -vector space

Given Let strictly ordered integral rings R A and be an Archimedean ordered pointed S \mathbb{Q} , -vector a space monotonic and commutative let ring homomorphism$h:R \to S$ is strictly monotonic if for all $a:R$ and $b:R$, $a \lt b$ implies $h(a) \lt h(b)$.

Every strictly ordered ring $R$ has a strictly monotonic commutative ring homomorphism $h:\mathbb{Z} \to R$ from the integers to $R$, and there is an strictly monotonic injection $i:\mathbb{Z}_+ \to \mathbb{Z}$ from the positive integers to the integers.

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

A be strictly the ordered positive integral elements ring in R A . is a strictly ordered integral \mathbb{Q} A -algebra if there is a function$j:\mathbb{Z}_+ \to R$sequentially Cauchy complete such if that every for Cauchy all sequence positive in integers a:\mathbb{Z}_+ A , converges:$h(i(a)) \cdot j(a) = 1$.

### Archimedean ordered integral $\mathbb{Q}$-algebras

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

A strictly ordered integral $\mathbb{Q}$-algebra $A$ is an Archimedean ordered integral $\mathbb{Q}$-algebra if for all elements $a:A$ and $b:A$, if $a \lt b$, then there merely exists a rational number $q:\mathbb{Q}$ such that $a \lt h(q)$ and $h(q) \lt b$.

$\forall x: \mathbb{N} \to A. isCauchy(x) \wedge \exists l \in A. isLimit(x, l)$

### Sequentially Cauchy complete Archimedean ordered integral $\mathbb{Q}$-algebras

Let $A$ be an Archimedean ordered integral $\mathbb{Q}$-algebra 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 13:11:18 by Anonymous?. See the history of this page for a list of all contributions to it.