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

Definition

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 March 31, 2022 at 02:43:40 by Anonymous?. See the history of this page for a list of all contributions to it.