Homotopy Type Theory Cauchy net > history (Rev #6, changes)

Showing changes from revision #5 to #6: Added | ~~Removed~~ | ~~Chan~~ged

Definition
See also

Definition

In premetric spaces

Let $T$ be a directed type, and let $S$ be a $T$ -premetric space. Given a directed type $I$ , a net $x: I \to S$ is a Cauchy net if

x:I \to S \vdash c(x):\prod_{\epsilon:T} \Vert \sum_{N:I} \prod_{i:I} \prod_{j:I} (i \geq N) \times (j \geq N) \times (x_i \sim_{\epsilon} x_j) \Vert

Cauchy approximations

Let $R T$ R T be a ~~Archimedean~~ directed ~~ordered~~ type ~~integral~~ ~~domain~~ ~~with~~ and a ~~dense~~ codirected type where the directed type operation~~strict order~~ $\oplus$ , is associative, and let $R_{+} S$ ~~R_{+}~~ S be ~~the~~ a~~semiring?~~ $T$ - of ~~positive~~ ~~terms~~ in ~~$R$~~ premetric space . If A ~~both~~ net $x : T \to S$ x: T \to S ~~and~~ is a ~~$I$~~ $T$ -Cauchy approximation ~~are~~ ~~$R_{+}$~~ ~~, then a net~~ ~~$x: R_{+} \to S$~~ ~~is a~~ ~~Cauchy approximation~~ if

x : R_{+} \to S ⊢ c (x) : \prod_{δ : R_{+}} \prod_{η : R_{+}} x_{δ} \sim_{δ + \oplus η} x_{η}

x:R_{+} \to S \vdash c(x):\prod_{\delta:R_{+}} \prod_{\eta:R_{+}} x_\delta \sim_{\delta + \oplus \eta} x_\eta

Every $T$ -Cauchy approximation is a Cauchy net indexed by $T$ . This is because $T$ is a codirected type, with $N:T$ defined as $N \coloneqq \delta \otimes \eta$ for $\delta:T$ and $\eta:T$ . $\epsilon:R_{+}$ is defined as $\epsilon \coloneqq \delta \oplus \eta$ .

In Cauchy spaces

…

Cauchy sequences

A Cauchy sequence is a Cauchy net whose index type is the natural numbers $\mathbb{N}$ .