Homotopy Type Theory
HoTT book real numbers > history (Rev #10)
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 premetric space is a set S S with a ternary relation ∼ \sim on the Cartesian product ℚ + × S × S \mathbb{Q}_{+} \times S \times S , where
ℚ + ≔ { x ∈ ℚ | 0 < x } \mathbb{Q}_{+} \coloneqq \{x \in \mathbb{Q} \vert 0 \lt x\}
is the set of positive rational numbers. A Cauchy approximation in S S is an function x ∈ S ℚ + x \in S^{\mathbb{Q}_{+}} , where S ℚ + S^{\mathbb{Q}_{+}} is the set of functions with domain ℚ + \mathbb{Q}_{+} and codomain S S , such that
∀ δ ∈ ℚ + . ∀ η ∈ ℚ + . x ( δ ) ∼ δ + η x ( η ) \forall \delta \in \mathbb{Q}_{+}.\forall \eta \in \mathbb{Q}_{+}.x(\delta) \sim_{\delta + \eta} x(\eta)
The set of all Cauchy approximations is defined as
C ( S ) ≔ { x ∈ S ℚ + | ∀ δ ∈ ℚ + . ∀ η ∈ ℚ + . x ( δ ) ∼ δ + η x ( η ) } C(S) \coloneqq \{x \in S^{\mathbb{Q}_{+}} \vert \forall \delta \in \mathbb{Q}_{+}.\forall \eta \in \mathbb{Q}_{+}.x(\delta) \sim_{\delta + \eta} x(\eta)\}
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)} 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 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 13, 2022 at 22:01:03 by
Anonymous? .
See the history of this page for a list of all contributions to it.