# 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 Cauchy complete if every Cauchy net in $F$ converges:

$\prod_{I:\mathcal{U}} isDirected(I) \times \prod_{x:I \to F} isCauchy(x) \times \Vert \sum_{l:F} isLimit(x, l) \Vert$

## Examples

• The type of real numbers $\mathbb{R}$ is a Cauchy complete Archimedean ordered field.