# Homotopy Type Theory sequentially Cauchy complete Archimedean ordered field > history (changes)

Showing changes from revision #2 to #3: Added | Removed | Changed

# Contents

## Definition

Let $F$ be an Archimedean ordered field and let

$F_{+} \coloneqq \sum_{a:F} 0 \lt a$

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

$isCauchy(x) \coloneqq \forall \epsilon \in F_{+}. \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 F_{+}. \exists N \in I. \forall i \in I. (i \geq N) \to (\vert x_i - l \vert \lt \epsilon)$
$\forall x \in F^\mathbb{N}. isCauchy(x) \wedge \exists l \in F. isLimit(x, l)$