## Definition ## Let $R$ be a [[Archimedean ordered integral domain]] with a [[dense linear order]], and let $R_{+}$ be the [[semiring]] of positive terms in $R$. A __$R_{+}$-Cauchy structure__ is a $R_{+}$-premetric space $S$ with * a function $inj: R \to S$ * a function $lim: C(S, R_{+}) \to S$, where $C(S, R_{+})$ is the type of $R_{+}$-[[Cauchy approximation]]s in $S$ * dependent families of terms $$a:S, b:S \vdash eq(a, b): \Vert \prod_{\epsilon:R_{+}} (a \sim_{\epsilon} b) \Vert \to (a =_S b)$$ $$a:R, b:R, \epsilon:R_{+} \vdash \mu_{R, R}(a, b, \epsilon): (\vert a - b \vert \lt \epsilon) \to (inj(a) \sim_{\epsilon} inj(b))$$ $$a:R, b:C_{S}(R_{+}), \epsilon:R_{+}, \eta:R_{+} \vdash \mu_{R, C(S, R_{+})}(a, b, \epsilon, \eta): (inj(a) \sim_{\epsilon} b_{\eta}) \to (inj(a) \sim_{\delta + \eta} lim(b))$$ $$a:C(S, R_{+}), b:R, \delta:R_{+}, \epsilon:R_{+} \vdash \mu_{C(S, R_{+}), R}(a, b, \delta, \epsilon): (a_{\delta} \sim_{\epsilon} inj(b) ) \to (lim(a) \sim_{\delta + \epsilon} inj(b))$$ $$a:C(S, R_{+}), b:C(S, R_{+}), \delta:R_{+}, \epsilon:R_{+}, \eta:R_{+} \vdash \mu_{C(S, R_{+}), C(S, R_{+})}(a, b, \delta, \epsilon, \eta): (a_{\delta} \sim_{\epsilon} b_{\eta} ) \to (lim(a) \sim_{\delta + \epsilon + \eta} lim(b))$$ For two $R_{+}$-Cauchy structures $S$ and $T$, a __$R_{+}$-Cauchy structure homomorphism__ consists of * a function $f:S \to T$ * a dependent family of functions $$a:S, b:S, \epsilon:R_{+} \vdash \pi(a, b, \epsilon): (a \sim_{S\epsilon} b) \to (f(a) \sim_{T\epsilon} f(b))$$ * a dependent family of types $$r:R \vdash \iota(r): f(inj_S(r)) = inj_T(r)$$ * a dependent family of types $$r:C(S, R_{+}) \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:R_{+}} (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](https://etheses.bham.ac.uk/id/eprint/10411/7/Booij2020PhD.pdf))