Homotopy Type Theory
HoTT book real numbers > history (Rev #11, changes)
Showing changes from revision #10 to #11:
Added | Removed | Changed
Contents
Whenever editing is allowed on the nLab again, this article should be ported over there.
Definition
Let R R be a dense integral subdomain of the rational numbers ℚ \mathbb{Q} and let R + R_{+} be the positive terms of R R . The HoTT book real numbers ℝ H \mathbb{R}_H are a homotopy initial R + R_{+} -Cauchy structure , i.e. an R + R_{+} -Cauchy structure such that for every other R + R_{+} -Cauchy structure S S , the type of R + R_{+} -Cauchy structure homomorphisms with domain ℝ H \mathbb{R}_H and codomain S S is contractible .
As a higher inductive-inductive type
Let R R be a dense integral subdomain of the rational numbers ℚ \mathbb{Q} and let R + R_{+} be the positive terms of R R . The HoTT book real numbers ℝ H \mathbb{R}_H are inductively generated by the following:
a function inj : R → ℝ H inj: R \to \mathbb{R}_H
a function lim : C ( ℝ H , R + ) → ℝ H lim: C(\mathbb{R}_H, R_{+}) \to \mathbb{R}_H , where C ( ℝ H , R + ) C(\mathbb{R}_H, R_{+}) is the type of R + R_{+} -indexed net s in ℝ H \mathbb{R}_H that are R + R_{+} -Cauchy approximation s.
a dependent family of terms
a : ℝ H , b : ℝ H ⊢ eq ℝ H ( a , b ) : ( ∏ ϵ : R + ( a ∼ ϵ b ) ) → ( a = ℝ H b ) a:\mathbb{R}_H, b:\mathbb{R}_H \vdash eq_{\mathbb{R}_H}(a, b): \left( \prod_{\epsilon:R_{+}} (a \sim_{\epsilon} b) \right) \to (a =_{\mathbb{R}_H} b)
and the R + R_{+} -premetric type family ∼ \sim is simultaneously inductively generated by the following:
a dependent family of terms
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 dependent family of terms
a : R , b : C ( ℝ H , R + ) , ϵ : R + , η : R + ⊢ μ R , C ( ℝ H , R + ) ( a , b , ϵ , η ) : ( inj ( a ) ∼ ϵ b η ) → ( inj ( a ) ∼ ϵ + η lim ( b ) ) a:R, b:C(\mathbb{R}_H, R_{+}), \epsilon:R_{+}, \eta:R_{+} \vdash \mu_{R, C(\mathbb{R}_H, R_{+})}(a, b, \epsilon, \eta): (inj(a) \sim_{\epsilon} b_{\eta}) \to (inj(a) \sim_{\epsilon + \eta} lim(b))
a dependent family of terms
a : C ( ℝ H , R + ) , b : R , δ : R + , ϵ : R + ⊢ μ C ( ℝ H , R + ) , R ( a , b , δ , ϵ ) : ( a δ ∼ ϵ inj ( b ) ) → ( lim ( a ) ∼ δ + ϵ inj ( b ) ) a:C(\mathbb{R}_H, R_{+}), b:R, \delta:R_{+}, \epsilon:R_{+} \vdash \mu_{C(\mathbb{R}_H, R_{+}), R}(a, b, \delta, \epsilon): (a_{\delta} \sim_{\epsilon} inj(b) ) \to (lim(a) \sim_{\delta + \epsilon} inj(b))
a dependent family of terms
a : C ( ℝ H , R + ) , b : C ( ℝ H , R + ) , δ : R + , ϵ : R + , η : R + ⊢ μ C ( ℝ H , R + ) , C ( ℝ H , R + ) ( a , b , δ , ϵ , η ) : ( a δ ∼ ϵ b η ) → ( lim ( a ) ∼ δ + ϵ + η lim ( b ) ) a:C(\mathbb{R}_H, R_{+}), b:C(\mathbb{R}_H, R_{+}), \delta:R_{+}, \epsilon:R_{+}, \eta:R_{+} \vdash \mu_{C(\mathbb{R}_H, R_{+}), C(\mathbb{R}_H, R_{+})}(a, b, \delta, \epsilon, \eta): (a_{\delta} \sim_{\epsilon} b_{\eta} ) \to (lim(a) \sim_{\delta + \epsilon + \eta} lim(b))
a dependent family of terms
a : R , b : R , ϵ : R + ⊢ π ( a , b , ϵ ) : isProp ( a ∼ ϵ b ) a:R, b:R, \epsilon:R_{+} \vdash \pi(a, b, \epsilon): isProp(a \sim_{\epsilon} b)
In set theory
A The set of premetric HoTT space book real numbers is a setS ℝ H S \mathbb{R}_H with is a the ternary initial relation object in the ∼ \sim category of Cauchy structures on and the Cartesian product ℚ + × S × S \mathbb{Q}_{+} \times S \times S Cauchy structure homomorphism , s. where
ℚ + ≔ { x ∈ ℚ | 0 < x } \mathbb{Q}_{+} \coloneqq \{x \in \mathbb{Q} \vert 0 \lt x\} In homotopy type theory is The the set of positive rational numbers. A Cauchy HoTT approximation book real numbers inS ℝ H S \mathbb{R}_H is are an a function homotopy initial x ∈ S ℚ + x \in S^{\mathbb{Q}_{+}} Cauchy structure , where i.e. a Cauchy structure such that for every other Cauchy structure S ℚ + S S^{\mathbb{Q}_{+}} S , is the set type of functions with domainℚ + \mathbb{Q}_{+} Cauchy structure homomorphism s and with codomain domain S ℝ H S \mathbb{R}_H , such and that codomain S S is contractible .
∀ δ ∈ ℚ + . ∀ η ∈ ℚ + . x ( δ ) ∼ δ + η x ( η ) \forall \delta \in \mathbb{Q}_{+}.\forall \eta \in \mathbb{Q}_{+}.x(\delta) \sim_{\delta + \eta} x(\eta) As a higher inductive-inductive type The Let set of all Cauchy approximations is defined asℚ \mathbb{Q} be the rational numbers and let
C ℚ + ( S ) ≔ { ∑ x : ℚ 0 < x ∈ S ℚ + | ∀ δ ∈ ℚ + . ∀ η ∈ ℚ + . x ( δ ) ∼ δ + η x ( η ) } C(S) \mathbb{Q}_{+} \coloneqq \{x \sum_{x:\mathbb{Q}} \in 0 S^{\mathbb{Q}_{+}} \lt \vert x \forall \delta \in \mathbb{Q}_{+}.\forall \eta \in \mathbb{Q}_{+}.x(\delta) \sim_{\delta + \eta} x(\eta)\}
A be the positive rational numbers. The Cauchy HoTT structure book real numbers is a premetric spaceS ℝ H S \mathbb{R}_H with are a inductively function generated by the following: 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 ∼ ϵ b ) ⇒ a = b ) \forall a \in S.\forall b \in S.((\forall \epsilon \in \mathbb{Q}_{+}.a \sim_\epsilon b) \implies a = b)
a function inj : ℚ → ℝ H inj: \mathbb{Q} \to \mathbb{R}_H
a function lim : C ( ℝ H ) → ℝ H lim: C(\mathbb{R}_H) \to \mathbb{R}_H , where C ( ℝ H ) C(\mathbb{R}_H) is the type of Cauchy approximation s in ℝ H \mathbb{R}_H .
a dependent family of terms
∀ 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 ∈ : ℚ ℝ H . , ∀ b ∈ : C ℝ H ⊢ eq ℝ H ( S ) . ∀ ϵ ∈ ℚ + . ∀ η ∈ ℚ + . ( rat ( a ) , ∼ ϵ b ( η ) ⇒ : rat ( ∏ ϵ : ℚ + ( a ∼ ϵ b ) ) → ( a ) = ℝ H ∼ ϵ + η lim ( b ) ) \forall a:\mathbb{R}_H, a b:\mathbb{R}_H \in \vdash \mathbb{Q}.\forall eq_{\mathbb{R}_H}(a, b b): \in \left( C(S).\forall \prod_{\epsilon:\mathbb{Q}_{+}} \epsilon (a \in \sim_{\epsilon} \mathbb{Q}_{+}.\forall b) \eta \right) \in \to \mathbb{Q}_{+}.(rat(a) (a \sim_\epsilon =_{\mathbb{R}_H} b(\eta) b) \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)) and the premetric type family ∼ \sim is simultaneously inductively generated by the following:
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 dependent family of terms
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 dependent family of terms
a : ℚ , b : C ( ℝ H ) , ϵ : ℚ + , η : ℚ + ⊢ μ ℚ , C ( ℝ H ) ( a , b , ϵ , η ) : ( inj ( a ) ∼ ϵ b η ) → ( inj ( a ) ∼ ϵ + η lim ( b ) ) a:\mathbb{Q}, b:C(\mathbb{R}_H), \epsilon:\mathbb{Q}_{+}, \eta:\mathbb{Q}_{+} \vdash \mu_{\mathbb{Q}, C(\mathbb{R}_H)}(a, b, \epsilon, \eta): (inj(a) \sim_{\epsilon} b_{\eta}) \to (inj(a) \sim_{\epsilon + \eta} lim(b))
a dependent family of terms
a : C ( ℝ H ) , b : ℚ , δ : ℚ + , ϵ : ℚ + ⊢ μ C ( ℝ H ) , ℚ ( a , b , δ , ϵ ) : ( a δ ∼ ϵ inj ( b ) ) → ( lim ( a ) ∼ δ + ϵ inj ( b ) ) a:C(\mathbb{R}_H), b:\mathbb{Q}, \delta:\mathbb{Q}_{+}, \epsilon:\mathbb{Q}_{+} \vdash \mu_{C(\mathbb{R}_H), \mathbb{Q}}(a, b, \delta, \epsilon): (a_{\delta} \sim_{\epsilon} inj(b) ) \to (lim(a) \sim_{\delta + \epsilon} inj(b))
a dependent family of terms
a : C ( ℝ H ) , b : C ( ℝ H ) , δ : ℚ + , ϵ : ℚ + , η : ℚ + ⊢ μ C ( ℝ H ) , C ( ℝ H ) ( a , b , δ , ϵ , η ) : ( a δ ∼ ϵ b η ) → ( lim ( a ) ∼ δ + ϵ + η lim ( b ) ) a:C(\mathbb{R}_H), b:C(\mathbb{R}_H), \delta:\mathbb{Q}_{+}, \epsilon:\mathbb{Q}_{+}, \eta:\mathbb{Q}_{+} \vdash \mu_{C(\mathbb{R}_H), C(\mathbb{R}_H)}(a, b, \delta, \epsilon, \eta): (a_{\delta} \sim_{\epsilon} b_{\eta} ) \to (lim(a) \sim_{\delta + \epsilon + \eta} lim(b))
a dependent family of terms
a : ℚ , b : ℚ , ϵ : ℚ + ⊢ π ( a , b , ϵ ) : isProp ( a ∼ ϵ b ) a:\mathbb{Q}, b:\mathbb{Q}, \epsilon:\mathbb{Q}_{+} \vdash \pi(a, b, \epsilon): isProp(a \sim_{\epsilon} b)
∀ 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 set of HoTT book real numbers ℝ H \mathbb{R}_H is the initial object in the category of Cauchy structures and Cauchy structure homomorphisms.
See also
References
Revision on April 14, 2022 at 00:15:05 by
Anonymous? .
See the history of this page for a list of all contributions to it.