[[!redirects Cauchy structure homomorphism]] [[!redirects category of Cauchy structures]] #Contents# * table of contents {:toc} Whenever editing is allowed on the [[nLab:HomePage|nLab]] again, this article should be ported over there. ## Definition ## ### In set theory ### Let $\mathbb{Q}$ be the [[rational numbers]] and let $$\mathbb{Q}_{+} \coloneqq \{x \in \mathbb{Q} \vert 0 \lt x\}$$ 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 approximation]]s in $S$, such that $$\forall a \in S.\forall b \in S.((\forall \epsilon \in \mathbb{Q}_{+}.a \sim_\epsilon b) \implies a = b)$$ $$\forall a \in \mathbb{Q}.\forall b \in \mathbb{Q}.\forall \epsilon \in \mathbb{Q}_{+}.(\vert a - b \vert \lt \epsilon \implies rat(a) \sim_\epsilon rat(b))$$ $$\forall a \in \mathbb{Q}.\forall b \in C(S).\forall \epsilon \in \mathbb{Q}_{+}.\forall \eta \in \mathbb{Q}_{+}.(rat(a) \sim_\epsilon b(\eta) \implies rat(a) \sim_{\epsilon + \eta} lim(b))$$ $$\forall a \in C(S).\forall b \in \mathbb{Q}.\forall \epsilon \in \mathbb{Q}_{+}.\forall \delta \in \mathbb{Q}_{+}.(a(\delta) \sim_\epsilon rat(b) \implies lim(a) \sim_{\delta + \epsilon} rat(b))$$ $$\forall a \in C(S).\forall b \in C(S).\forall \epsilon \in \mathbb{Q}_{+}.\forall \delta \in \mathbb{Q}_{+}.\forall \eta \in \mathbb{Q}_{+}.(a(\delta) \sim_\epsilon b(\eta) \implies lim(a) \sim_{\delta + \epsilon + \eta} lim(b))$$ For two Cauchy structures $S$ and $T$, a __Cauchy structure homomorphism__ is a function $f\in T^S$ such that $$\forall a \in S.\forall b \in S.\forall \epsilon \in \mathbb{Q}_{+}.(a \sim_{\epsilon} b) \to (f(a) \sim_{\epsilon} f(b))$$ $$\forall r\in \mathbb{Q}.f(rat(r)) = rat(r)$$ $$\forall r\in C(S).f(lim(r)) = lim(f \circ r)$$ $$\forall a \in S.\forall b \in S.(((\forall \epsilon \in \mathbb{Q}_{+}.a \sim_\epsilon b) \implies a = b) \implies ((\forall \epsilon \in \mathbb{Q}_{+}.f(a) \sim_\epsilon f(b)) \implies f(a) = f(b))$$ 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 $$\mathbb{Q}_{+} \coloneqq \sum_{x:\mathbb{Q}} 0 \lt x$$ 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 approximation]]s in $S$ * dependent families of terms $$a:S, b:S \vdash eq(a, b): \Vert \prod_{\epsilon:\mathbb{Q}_{+}} (a \sim_{\epsilon} b) \Vert \to (a =_S b)$$ $$a:\mathbb{Q}, b:\mathbb{Q}, \epsilon:\mathbb{Q}_{+} \vdash \mu_{\mathbb{Q}, \mathbb{Q}}(a, b, \epsilon): (\vert a - b \vert \lt \epsilon) \to (inj(a) \sim_{\epsilon} inj(b))$$ $$a:\mathbb{Q}, b:C(S), \epsilon:\mathbb{Q}_{+}, \eta:\mathbb{Q}_{+} \vdash \mu_{\mathbb{Q}, C(S)}(a, b, \epsilon, \eta): (inj(a) \sim_{\epsilon} b_{\eta}) \to (inj(a) \sim_{\epsilon + \eta} lim(b))$$ $$a:C(S), b:\mathbb{Q}, \delta:\mathbb{Q}_{+}, \epsilon:\mathbb{Q}_{+} \vdash \mu_{C(S), \mathbb{Q}}(a, b, \delta, \epsilon): (a_{\delta} \sim_{\epsilon} inj(b) ) \to (lim(a) \sim_{\delta + \epsilon} inj(b))$$ $$a:C(S), b:C(S), \delta:\mathbb{Q}_{+}, \epsilon:\mathbb{Q}_{+}, \eta:\mathbb{Q}_{+} \vdash \mu_{C(S), C(S)}(a, b, \delta, \epsilon, \eta): (a_{\delta} \sim_{\epsilon} b_{\eta} ) \to (lim(a) \sim_{\delta + \epsilon + \eta} lim(b))$$ 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](https://etheses.bham.ac.uk/id/eprint/10411/7/Booij2020PhD.pdf))