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


Whenever editing is allowed on the nLab again, this article should be ported over there.


In set theory

Let \mathbb{Q} be the rational numbers and let

+{x|0<x}\mathbb{Q}_{+} \coloneqq \{x \in \mathbb{Q} \vert 0 \lt x\}

be the set of positive rational numbers. Let II be a directed set and

C(I,){x I|ϵ +.NI.iI.jI.(iN)(jN)(x i ϵx j)}C(I, \mathbb{Q}) \coloneqq \{x \in \mathbb{Q}^I \vert \forall \epsilon \in \mathbb{Q}_{+}. \exists N \in I. \forall i \in I. \forall j \in I. (i \geq N) \wedge (j \geq N) \wedge (x_i \sim_{\epsilon} x_j)\}

is the set of all Cauchy nets with index set II and values in \mathbb{Q}. Let

CauchyNetsIn() IOb(DirectedSet 𝒰)C(I,)CauchyNetsIn(\mathbb{Q}) \coloneqq \bigcup_{I \in Ob(DirectedSet_\mathcal{U})} C(I, \mathbb{Q})

be the (large) set of all Cauchy nets in \mathbb{Q} in a universe 𝒰\mathcal{U}, where DirectedSet 𝒰DirectedSet_\mathcal{U} is the category of all directed sets in 𝒰\mathcal{U}.

Let the relation I,J\equiv_{I, J} in the Cartesian product C(I,)×C(J,)C(I, \mathbb{Q}) \times C(J, \mathbb{Q}) for directed sets II and JJ be defined as

a I,Jbϵ +,MI.iI.NJ.jJ.(iM)(jN)(|a ib j|<ϵ)a \equiv_{I, J} b \coloneqq \forall \epsilon \in \mathbb{Q}_{+}, \exists M \in I. \forall i \in I. \exists N \in J. \forall j \in J. (i \geq M) \wedge (j \geq N) \wedge (\vert a_i - b_j \vert \lt \epsilon)

Let a generalized Cauchy algebra be defined as a set AA with a function ιA CauchyNetsIn()\iota \in {A}^{CauchyNetsIn(\mathbb{Q})} such that

IOb(DirectedSet 𝒰).JOb(DirectedSet 𝒰).aC(I,).bC(J,).(a I,Jb)(ι(a)=ι(b))\forall I \in Ob(DirectedSet_\mathcal{U}). \forall J \in Ob(DirectedSet_\mathcal{U}). \forall a \in C(I, \mathbb{Q}). \forall b \in C(J, \mathbb{Q}). (a \equiv_{I, J} b) \implies (\iota(a) = \iota(b))

A generalized Cauchy algebra homomorphism is a function f:B Af:B^A between Cauchy algebras AA and BB such that

aC().f(ι A(a))=ι B(a)\forall a \in C(\mathbb{Q}). f(\iota_A(a)) = \iota_B(a)

The category of generalized Cauchy algebras is the category GCAlgGCAlg whose objects Ob(GCAlg)Ob(GCAlg) are generalized Cauchy algebras and whose morphisms Mor(GCAlg)Mor(GCAlg) are generalized Cauchy algebra homomorphisms. The set of generalized Cauchy real numbers, denoted \mathbb{R}, is defined as the initial object in the category of Cauchy algebras.

In homotopy type theory

Let \mathbb{Q} be the rational numbers and let

+ x:0<x\mathbb{Q}_{+} \coloneqq \sum_{x:\mathbb{Q}} 0 \lt x

be the positive rational numbers.

The generalized Cauchy real numbers 𝒰\mathbb{R}_\mathcal{U} are inductively generated by the following:

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

    C(I,)isDirected(I)× x:IisCauchy(x)C(I, \mathbb{Q}) \coloneqq isDirected(I) \times \sum_{x:I \to \mathbb{Q}} isCauchy(x)

    is the type of all Cauchy nets with index type II and values in \mathbb{Q}.

  • a dependent family of terms

    a:C(I,),b:C(J,)eq 𝒰(a,b):isEq 𝒰(a,b)(ι(a)= 𝒰ι(b))a:C(I, \mathbb{Q}), b:C(J, \mathbb{Q}) \vdash eq_{\mathbb{R}_\mathcal{U}}(a, b): isEq_{\mathbb{R}_\mathcal{U}}(a, b) \to (\iota(a) =_{\mathbb{R}_\mathcal{U}} \iota(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) ϵ: + M:I i:I N:J j:J(iM)×(jN)×(|a ib j|<ϵ)isEq_{\mathbb{R}_\mathcal{U}}(a, b) \coloneqq \prod_{\epsilon:\mathbb{Q}_{+}} \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 April 14, 2022 at 15:38:51 by Anonymous?. See the history of this page for a list of all contributions to it.