Homotopy Type Theory Cauchy structure > history (Rev #9)

Definition

Let $A$ be a dense Archimedean ordered abelian group with a point $1:A$ and a term $\zeta: 0 \lt 1$. Let $A_{+} \coloneqq \sum_{a:A} (0 \lt a)$ be the positive cone? of $A$.

A $A_{+}$-Cauchy structure is a $A_{+}$-premetric space $S$ with

• a function $inj: A \to S$

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

• dependent families of terms

For two $A_{+}$-Cauchy structures $S$ and $T$, a $A_{+}$-Cauchy structure homomorphism consists of

• a function $f:S \to T$

• a dependent family of functions

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

• a dependent family of types

  $$r:A \vdash \iota(r): f(inj_S(r)) = inj_T(r)$$

• a dependent family of types

  $$r:C(S, A_{+}) \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:A_{+}} (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
• HoTT book real numbers

References

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