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

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

Definition

A Cauchy structure is a premetric space $S$ with a function $rat \in S^{\mathbb{Q}_{+}}$ and a function $lim \in S^{C(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))

Let $R$ be a dense integral subdomain of the rational numbers $\mathbb{Q}$ and let $R_{+}$ be the positive terms of $R$ .

An $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 approximations 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_{\epsilon + \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))$

Revision on April 13, 2022 at 22:00:44 by Anonymous?. See the history of this page for a list of all contributions to it.