Homotopy Type Theory HoTT book real numbers > history (Rev #6)

Definition

Let RR be a dense integral subdomain of the rational numbers \mathbb{Q} and let R +R_{+} be the positive terms of RR. 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 SS, the type of R +R_{+}-Cauchy structure homomorphisms with domain H\mathbb{R}_H and codomain SS is contractible.

As a higher inductive-inductive type

Let RR be a dense integral subdomain of the rational numbers \mathbb{Q} and let R +R_{+} be the positive terms of RR. The HoTT book real numbers H\mathbb{R}_H are inductively generated by the following:

  • a function inj:R Hinj: R \to \mathbb{R}_H

  • a function lim:C( H,R +) Hlim: 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 nets in H\mathbb{R}_H that are R +R_{+}-Cauchy approximations.

  • a dependent family of terms

a: H,b: Heq H(a,b):( ϵ:R +(a ϵb))(a= Hb)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,ϵ):(|ab|<ϵ)(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 01:47:18 by Anonymous?. See the history of this page for a list of all contributions to it.