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

Showing changes from revision #8 to #9: Added | ~~Removed~~ | ~~Chan~~ged

Definition

Let $R A$ R A be a ~~Archimedean ordered integral domain~~ ~~with a~~ dense ~~strict~~ Archimedean ~~order~~ ordered abelian group , ~~and~~ with ~~let~~ a point $R_{+} 1 : A$ ~~R_{+}~~ 1:A be and ~~the~~ a term~~semiring?~~ $\zeta: 0 \lt 1$ . of Let ~~positive~~ ~~terms~~ in $R A_{+} ≔ \sum_{a : A} (0 < a)$ R A_{+} \coloneqq \sum_{a:A} (0 \lt a) be the positive cone? of $A$ .

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

$a : S, b : S, c : ‖ \prod_{ϵ : {R A}_{+}} (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:R_{+}}~~ \prod_{\epsilon:A_{+}} (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 12, 2022 at 22:13:42 by Anonymous?. See the history of this page for a list of all contributions to it.

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

Definition

See also

References