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

Showing changes from revision #10 to #11: Added | ~~Removed~~ | ~~Chan~~ged

Definition

Let $A R$ A R be a dense integral subdomain of the ~~dense~~ rational numbers ~~Archimedean ordered abelian group~~ $\mathbb{Q}$ ~~with~~ and a let ~~point~~ $1 R_{+} : A$ ~~1:A~~ R_{+} ~~and~~ be a the ~~term~~ positive terms of $ζ R : 0 < 1$ ~~\zeta:~~ R 0 ~~\lt~~ 1~~. Let~~ ~~$A_{+} \coloneqq \sum_{a:A} (0 \lt a)$~~ ~~be the~~ ~~positive cone?~~ of ~~$A$~~ ~~with respect to~~ ~~$0$~~ .

A An ${A R}_{+}$ ~~A_{+}~~ R_{+}-Cauchy structure is a ${A R}_{+}$ ~~A_{+}~~ R_{+}-premetric space $S$ with

a function $inj : A R \to S$ inj: A R \to S
a function $\lim : C (S, {A R}_{+}) \to S$ lim: C(S, ~~A_{+})~~ R_{+}) \to S, where $C (S, {A R}_{+})$ C(S, ~~A_{+})~~ R_{+}) is the type of ${A R}_{+}$ ~~A_{+}~~ R_{+}-Cauchy approximations in $S$
dependent families of terms

a : S, b : S ⊢ eq (a, b) : ‖ \prod_{ϵ : {A R}_{+}} (a \sim_{ϵ} b) ‖ \to (a =_{S} b)

a:S, b:S \vdash eq(a, b): \Vert ~~\prod_{\epsilon:A_{+}}~~ \prod_{\epsilon:R_{+}} (a \sim_{\epsilon} b) \Vert \to (a =_S b)

a : A R, b : A R, ϵ : {A R}_{+} ⊢ μ_{A R, A R} (a, b, ϵ) : (| a - b | < ϵ) \to (inj (a) \sim_{ϵ} inj (b))

~~a:A,~~ a:R, ~~b:A,~~ b:R, ~~\epsilon:A_{+}~~ \epsilon:R_{+} \vdash ~~\mu_{A,~~ \mu_{R, ~~A}(a,~~ R}(a, b, \epsilon): (\vert a - b \vert \lt \epsilon) \to (inj(a) \sim_{\epsilon} inj(b))

a : A R, b : C_{S} (R_{+}), ϵ : {A R}_{+}, η : {A R}_{+} ⊢ μ_{A R, C (S, {A R}_{+})} (a, b, ϵ, η) : (inj (a) \sim_{ϵ} b_{η}) \to (inj (a) \sim_{ϵ + η} \lim (b))

~~a:A,~~ a:R, b:C_{S}(R_{+}), ~~\epsilon:A_{+},~~ \epsilon:R_{+}, ~~\eta:A_{+}~~ \eta:R_{+} \vdash ~~\mu_{A,~~ \mu_{R, C(S, ~~A_{+})}(a,~~ R_{+})}(a, b, \epsilon, \eta): (inj(a) \sim_{\epsilon} b_{\eta}) \to (inj(a) \sim_{\epsilon + \eta} lim(b))

a : C (S, {A R}_{+}), b : A R, δ : {A R}_{+}, ϵ : {A R}_{+} ⊢ μ_{C (S, {A R}_{+}), A R} (a, b, δ, ϵ) : (a_{δ} \sim_{ϵ} inj (b)) \to (\lim (a) \sim_{δ + ϵ} inj (b))

a:C(S, ~~A_{+}),~~ R_{+}), ~~b:A,~~ b:R, ~~\delta:A_{+},~~ \delta:R_{+}, ~~\epsilon:A_{+}~~ \epsilon:R_{+} \vdash \mu_{C(S, ~~A_{+}),~~ R_{+}), ~~A}(a,~~ R}(a, b, \delta, \epsilon): (a_{\delta} \sim_{\epsilon} inj(b) ) \to (lim(a) \sim_{\delta + \epsilon} inj(b))

a : C (S, {A R}_{+}), b : C (S, {A R}_{+}), δ : {A R}_{+}, ϵ : {A R}_{+}, η : R_{+} ⊢ μ_{C (S, {A R}_{+}), C (S, {A R}_{+})} (a, b, δ, ϵ, η) : (a_{δ} \sim_{ϵ} b_{η}) \to (\lim (a) \sim_{δ + ϵ + η} \lim (b))

a:C(S, ~~A_{+}),~~ R_{+}), b:C(S, ~~A_{+}),~~ R_{+}), ~~\delta:A_{+},~~ \delta:R_{+}, ~~\epsilon:A_{+},~~ \epsilon:R_{+}, \eta:R_{+} \vdash \mu_{C(S, ~~A_{+}),~~ R_{+}), C(S, ~~A_{+})}(a,~~ R_{+})}(a, b, \delta, \epsilon, \eta): (a_{\delta} \sim_{\epsilon} b_{\eta} ) \to (lim(a) \sim_{\delta + \epsilon + \eta} lim(b))

For two ${A R}_{+}$ ~~A_{+}~~ R_{+}-Cauchy structures $S$ and $T$ , a ${A R}_{+}$ ~~A_{+}~~ R_{+}-Cauchy structure homomorphism consists of

a function $f:S \to T$
a dependent family of functions

$a : S, b : S, ϵ : {A R}_{+} ⊢ π (a, b, ϵ) : (a \sim_{S ϵ} b) \to (f (a) \sim_{T ϵ} f (b))$ a:S, b:S, ~~\epsilon:A_{+}~~ \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 : A R ⊢ ι (r) : f ({inj}_{S} (r)) = {inj}_{T} (r)$ ~~r:A~~ r:R \vdash \iota(r): f(inj_S(r)) = inj_T(r)
a dependent family of types

$r : C (S, {A R}_{+}) ⊢ λ (r) : f (\lim_{S} (r)) = \lim_{T} (f \circ r)$ r:C(S, ~~A_{+})~~ R_{+}) \vdash \lambda(r): f(lim_S(r)) = lim_T(f \circ r)
a dependent family of types

$a : S, b : S, c : ‖ \prod_{ϵ : {A R}_{+}} (a \sim_{ϵ} b) ‖ ⊢ η (a, b, c) : f ({eq}_{S} (a, b, c)) = {eq}_{T} (f (a), f (b), f (c))$ a:S, b:S, c:\Vert ~~\prod_{\epsilon:A_{+}}~~ \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))

References

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

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.

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

Definition

See also

References