Homotopy Type Theory
Cauchy structure > history (Rev #13)
Contents
Whenever editing is allowed on the nLab again, this article should be ported over there.
Definition
In set theory
Let ℚ \mathbb{Q} be the rational numbers and let
ℚ + ≔ { x ∈ ℚ | 0 < x } \mathbb{Q}_{+} \coloneqq \{x \in \mathbb{Q} \vert 0 \lt x\}
be the set of positive rational numbers.
A Cauchy structure is a premetric space S S 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 approximation s in S 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 ∈ ℚ . ∀ 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)) ∀ 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))
For two Cauchy structures S S and T T , a Cauchy structure homomorphism is a function f ∈ T S f\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 CauchyStr CauchyStr 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 ℚ \mathbb{Q} be the rational numbers and let
ℚ + ≔ ∑ x : ℚ 0 < x \mathbb{Q}_{+} \coloneqq \sum_{x:\mathbb{Q}} 0 \lt x
be the positive rational numbers.
A Cauchy structure is a premetric space S S with
a function inj : ℚ → S inj: \mathbb{Q} \to S
a function lim : C ( S ) → S lim: C(S) \to S , where C ( S ) C(S) is the type of R + R_{+} -Cauchy approximation s in S S
dependent families of terms
a : S , b : S ⊢ eq ( a , b ) : ‖ ∏ ϵ : ℚ + ( a ∼ ϵ b ) ‖ → ( a = S b ) a:S, b:S \vdash eq(a, b): \Vert \prod_{\epsilon:\mathbb{Q}_{+}} (a \sim_{\epsilon} b) \Vert \to (a =_S 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)) 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 : 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 S S and T T , a Cauchy structure homomorphism consists of
a function f : S → T f: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.