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

Skip the Navigation Links | Home Page | All Pages | Latest Revisions | Authors |

Showing changes from revision #12 to #13: Added | Removed | Changed

Contents

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

Definition

In set theory

A LetCauchy structureℚ\mathbb{Q} is be a the premetric rational space numbers and letSS with a function rat∈S ℚ +rat \in S^{\mathbb{Q}_{+}} and a function lim∈S C(S)lim \in S^{C(S)} such that

∀a∈S.∀b∈S.((∀ϵ∈ℚ + . ≔a{∼ ϵxb∈)ℚ ⇒ |a0 = < b x ) } \forall \mathbb{Q}_{+} a \coloneqq \{x \in S.\forall \mathbb{Q} b \vert \in 0 S.((\forall \lt \epsilon x\} \in \mathbb{Q}_{+}.a \sim_\epsilon b) \implies a = b)
∀a∈ℚ.∀b∈ℚ.∀ϵ∈ℚ +.(|a−b|<ϵ⇒rat(a)∼ ϵrat(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))
∀a∈ℚ.∀b∈C(S).∀ϵ∈ℚ +.∀η∈ℚ +.(rat(a)∼ ϵb(η)⇒rat(a)∼ ϵ+ηlim(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))

be the set of positive rational numbers.

∀a∈C(S).∀b∈ℚ.∀ϵ∈ℚ +.∀δ∈ℚ +.(a(δ)∼ ϵrat(b)⇒lim(a)∼ δ+ϵrat(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))
∀a∈C(S).∀b∈C(S).∀ϵ∈ℚ +.∀δ∈ℚ +.∀η∈ℚ +.(a(δ)∼ ϵb(η)⇒lim(a)∼ δ+ϵ+ηlim(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))

A Cauchy structure is a premetric space SS with a function rat∈S ℚ +rat \in S^{\mathbb{Q}_{+}} and a function lim∈S C(S)lim \in S^{C(S)}, where C(S)C(S) is the set of Cauchy approximations in SS, such that

For two Cauchy structures SS and TT, a Cauchy structure homomorphism is a function f∈T Sf\in T^S such that

∀a∈S.∀b∈S.((∀ϵ∈ℚ +.a∼ ϵb)⇒a=b)\forall a \in S.\forall b \in S.((\forall \epsilon \in \mathbb{Q}_{+}.a \sim_\epsilon b) \implies a = b)
∀a∈ℚ.∀b∈ℚ.∀ϵ∈ℚ +.(|a−b|<ϵ⇒rat(a)∼ ϵrat(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))
∀a∈ S ℚ.∀b∈C(S).∀ϵ∈ℚ +.∀η∈ℚ +.(rat(a)∼ ϵb(η) → ⇒rat(f(a)∼ ϵϵ+η f lim(b)) \forall a \in S.\forall \mathbb{Q}.\forall b \in S.\forall C(S).\forall \epsilon \in \mathbb{Q}_{+}.(a \mathbb{Q}_{+}.\forall \sim_{\epsilon} \eta b) \in \to \mathbb{Q}_{+}.(rat(a) (f(a) \sim_\epsilon \sim_{\epsilon} b(\eta) f(b)) \implies rat(a) \sim_{\epsilon + \eta} lim(b))
∀ r a∈C(S).∀b∈ℚ.f∀ϵ∈ℚ +.∀δ∈ℚ +.(a(δ)∼ ϵrat( r b)⇒lim(a)=∼ δ+ϵrat( r b)) \forall r\in a \mathbb{Q}.f(rat(r)) \in = C(S).\forall rat(r) 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))
∀ r a∈C(S).f∀b∈C( lim S).∀ϵ∈ℚ +.∀δ∈ℚ +.∀η∈ℚ +.( r a(δ)∼ ϵb(η) = ⇒lim( f a ∘ )r∼ δ+ϵ+ηlim(b)) \forall r\in a C(S).f(lim(r)) \in = C(S).\forall lim(f b \circ \in r) 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))
∀a∈S.∀b∈S.(((∀ϵ∈ℚ +.a∼ ϵb)⇒a=b)⇒((∀ϵ∈ℚ +.f(a)∼ ϵf(b))⇒f(a)=f(b))\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))

For two Cauchy structures SS and TT, a Cauchy structure homomorphism is a function f∈T Sf\in T^S such that
∀a∈S.∀b∈S.∀ϵ∈ℚ +.(a∼ ϵb)→(f(a)∼ ϵf(b))\forall a \in S.\forall b \in S.\forall \epsilon \in \mathbb{Q}_{+}.(a \sim_{\epsilon} b) \to (f(a) \sim_{\epsilon} f(b))
∀r∈ℚ.f(rat(r))=rat(r)\forall r\in \mathbb{Q}.f(rat(r)) = rat(r)
∀r∈C(S).f(lim(r))=lim(f∘r)\forall r\in C(S).f(lim(r)) = lim(f \circ r)
∀a∈S.∀b∈S.(((∀ϵ∈ℚ +.a∼ ϵb)⇒a=b)⇒((∀ϵ∈ℚ +.f(a)∼ ϵf(b))⇒f(a)=f(b))\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 CauchyStrCauchyStr whose objects Ob(CauchyStr)Ob(CauchyStr) are Cauchy structures and whose morphisms Mor(A,B)Mor(A, B), for objects A∈Ob(CauchyStr)A \in Ob(CauchyStr) and B∈Ob(CauchyStr)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 R ℚ R \mathbb{Q} be a dense integral subdomain of therational numbers and letℚ\mathbb{Q} and let R +R_{+} be the positive terms of RR.

An R +R_{+}-Cauchy structure is a R +R_{+}-premetric space SS with

ℚ +≔∑ x:ℚ0<x\mathbb{Q}_{+} \coloneqq \sum_{x:\mathbb{Q}} 0 \lt x

  • a function inj:R→Sinj: R \to S

  • a function lim:C(S,R +)→Slim: C(S, R_{+}) \to S, where C(S,R +)C(S, R_{+}) is the type of R +R_{+}-Cauchy approximations in SS

  • dependent families of terms

be the positive rational numbers.

a:S,b:S⊢eq(a,b):‖∏ ϵ:R +(a∼ ϵb)‖→(a= Sb)a:S, b:S \vdash eq(a, b): \Vert \prod_{\epsilon:R_{+}} (a \sim_{\epsilon} b) \Vert \to (a =_S b)

A Cauchy structure is a premetric space SS with

a:R,b:R,ϵ:R +⊢μ R,R(a,b,ϵ):(|a−b|<ϵ)→(inj(a)∼ ϵinj(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 +),ϵ:R +,η:R +⊢μ R,C(S,R +)(a,b,ϵ,η):(inj(a)∼ ϵb η)→(inj(a)∼ ϵ+ηlim(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 function inj:ℚ→Sinj: \mathbb{Q} \to S

  • a function lim:C(S)→Slim: C(S) \to S, where C(S)C(S) is the type of R +R_{+}-Cauchy approximations in SS

  • dependent families of terms

a:C(S,R +),b:R,δ:R +,ϵ:R +⊢μ C(S,R +),R(a,b,δ,ϵ):(a δ∼ ϵinj(b))→(lim(a)∼ δ+ϵinj(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 +),δ:R +,ϵ:R +,η:R +⊢μ C(S,R +),C(S,R +)eq(a,b,δ,ϵ,η):‖∏ ϵ:ℚ +(a δa∼ ϵb ηb)‖→(lim(a)= S∼ δ+ϵ+ηlim(b)) a:C(S, a:S, R_{+}), b:S b:C(S, R_{+}), \delta:R_{+}, \epsilon:R_{+}, \eta:R_{+} \vdash \mu_{C(S, eq(a, R_{+}), b): C(S, \Vert R_{+})}(a, \prod_{\epsilon:\mathbb{Q}_{+}} b, (a \delta, \epsilon, \eta): (a_{\delta} \sim_{\epsilon} b_{\eta} b) ) \Vert \to (lim(a) (a \sim_{\delta =_S + b) \epsilon + \eta} lim(b))
a:ℚ,b:ℚ,ϵ:ℚ +⊢μ ℚ,ℚ(a,b,ϵ):(|a−b|<ϵ)→(inj(a)∼ ϵinj(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))

For two R +R_{+}-Cauchy structures SS and TT, a R +R_{+}-Cauchy structure homomorphism consists of

a:ℚ,b:C(S),ϵ:ℚ +,η:ℚ +⊢μ ℚ,C(S)(a,b,ϵ,η):(inj(a)∼ ϵb η)→(inj(a)∼ ϵ+ηlim(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:ℚ,δ:ℚ +,ϵ:ℚ +⊢μ C(S),ℚ(a,b,δ,ϵ):(a δ∼ ϵinj(b))→(lim(a)∼ δ+ϵinj(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 function f:S→Tf:S \to T

  • a dependent family of functions

    a:S,b:S,ϵ:R +⊢π(a,b,ϵ):(a∼ Sϵb)→(f(a)∼ Tϵf(b))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⊢ι(r):f(inj S(r))=inj T(r)r:R \vdash \iota(r): f(inj_S(r)) = inj_T(r)

  • a dependent family of types

    r:C(S,R +)⊢λ(r):f(lim S(r))=lim T(f∘r)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:‖∏ ϵ:R +(a∼ ϵ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_{+}} (a \sim_{\epsilon} b) \Vert \vdash \eta(a, b, c): f(eq_S(a, b, c)) = eq_T(f(a), f(b), f(c))
a:C(S),b:C(S),δ:ℚ +,ϵ:ℚ +,η:ℚ +⊢μ C(S),C(S)(a,b,δ,ϵ,η):(a δ∼ ϵb η)→(lim(a)∼ δ+ϵ+ηlim(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 SS and TT, a Cauchy structure homomorphism consists of

  • a function f:S→Tf:S \to T

  • a dependent family of functions

    a:S,b:S,ϵ:ℚ +⊢π(a,b,ϵ):(a∼ Sϵb)→(f(a)∼ Tϵf(b))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:ℚ⊢ι(r):f(inj S(r))=inj T(r)r:\mathbb{Q} \vdash \iota(r): f(inj_S(r)) = inj_T(r)

  • a dependent family of types

    r:C(S)⊢λ(r):f(lim S(r))=lim T(f∘r)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:‖∏ ϵ:ℚ +(a∼ ϵ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:\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

References

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

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

DiscussNext revision (to current)Previous revision (12 more)Current version of pageHide changesHistory (13 revisions)Rollback Source