Whenever editing is allowed on the nLab again, this article should be ported over there.

Definition

In set theory

Let $\mathbb{Q}$ be the rational numbers and let

be the set of positive rational numbers.

A Cauchy structure is a premetric space $S$ with a function $rat \in S^{\mathbb{Q}_{+}}$ and a function $lim \in S^{C(S)}$, where $C(S)$ is the set of Cauchy approximations in $S$, such that

For two Cauchy structures $S$ and $T$, a Cauchy structure homomorphism is a function $f\in T^S$ such that

The category of Cauchy structures is a category $CauchyStr$ whose objects $Ob(CauchyStr)$ are Cauchy structures and whose morphisms $Mor(A, B)$, for objects $A \in Ob(CauchyStr)$ and $B \in Ob(CauchyStr)$, are Cauchy structure homomorphisms. The initial object in the category of Cauchy structures is the HoTT book real numbers.

In homotopy type theory

Let $\mathbb{Q}$ be the rational numbers and let

be the positive rational numbers.

A Cauchy structure is a premetric space $S$ with

• a function $inj: \mathbb{Q} \to S$

• a function $lim: C(S) \to S$, where $C(S)$ is the type of $R_{+}$-Cauchy approximations in $S$

• dependent families of terms

For two Cauchy structures $S$ and $T$, a Cauchy structure homomorphism consists of

• a function $f:S \to T$

• a dependent family of functions

  $$a:S, b:S, \epsilon:\mathbb{Q}_{+} \vdash \pi(a, b, \epsilon): (a \sim_{S\epsilon} b) \to (f(a) \sim_{T\epsilon} f(b))$$

• a dependent family of types

  $$r:\mathbb{Q} \vdash \iota(r): f(inj_S(r)) = inj_T(r)$$

• a dependent family of types

  $$r:C(S) \vdash \lambda(r): f(lim_S(r)) = lim_T(f \circ r)$$

• a dependent family of types

  $$a:S, b:S, c:\Vert \prod_{\epsilon:\mathbb{Q}_{+}} (a \sim_{\epsilon} b) \Vert \vdash \eta(a, b, c): f(eq_S(a, b, c)) = eq_T(f(a), f(b), f(c))$$

See also

• premetric space
• Cauchy approximation
• Cauchy complete Archimedean ordered field
• HoTT book real numbers

References

• Auke B. Booij, Analysis in univalent type theory (pdf)