Homotopy Type Theory generalized Cauchy real numbers > history (Rev #2)

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 generalized Cauchy real numbers 𝒰\mathbb{R}_\mathcal{U} are inductively generated by the following:

  • a function inj:( I:𝒰C(I,R)) 𝒰inj: \left(\sum_{I:\mathcal{U}} C(I, R)\right) \to \mathbb{R}_\mathcal{U}, where

    C(I,R)isDirected(I)× x:IRisCauchy(x)C(I, R) \coloneqq isDirected(I) \times \sum_{x:I \to R} isCauchy(x)

    is the type of all Cauchy nets with index type II and values in RR.

  • a dependent family of terms

    a:C(I,R),b:C(J,R)eq 𝒰(a,b):isEq 𝒰(a,b)(inj(a)= 𝒰inj(b))a:C(I, R), b:C(J, R) \vdash eq_{\mathbb{R}_\mathcal{U}}(a, b): isEq_{\mathbb{R}_\mathcal{U}}(a, b) \to (inj(a) =_{\mathbb{R}_\mathcal{U}} inj(b))

    where II and JJ are directed types and the equivalence relation on Cauchy nets isEq 𝒰(a,b)isEq_{\mathbb{R}_\mathcal{U}}(a, b) is defined as

    isEq 𝒰(a,b) ϵ:R + M:I i:I N:J j:J(iM)×(jN)×(|a ib j|<ϵ)isEq_{\mathbb{R}_\mathcal{U}}(a, b) \coloneqq \prod_{\epsilon:R_{+}} \Vert \sum_{M:I} \prod_{i:I} \Vert \sum_{N:J} \prod_{j:J} (i \geq M) \times (j \geq N) \times (\vert a_i - b_j \vert \lt \epsilon) \Vert \Vert
  • a term τ:isSet( 𝒰)\tau: isSet(\mathbb{R}_\mathcal{U})

See also

Revision on March 31, 2022 at 03:13:54 by Anonymous?. See the history of this page for a list of all contributions to it.