Homotopy Type Theory
HoTT book real numbers > history (Rev #5, changes)
Showing changes from revision #4 to #5:
Added | Removed | Changed
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): \Vert \prod_{\epsilon:R_{+}} (a \sim_{\epsilon} b) \Vert \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)
See also
References
Revision on March 12, 2022 at 00:45:48 by
Anonymous? .
See the history of this page for a list of all contributions to it.