Homotopy Type Theory Cauchy approximation > history (Rev #11, changes)

Showing changes from revision #10 to #11: Added | ~~Removed~~ | ~~Chan~~ged

Definition
- In set theory
- In homotopy type theory
Properties
See also
References

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

Definition

~~Let $R$ be a dense integral subdomain of the rational numbers $\mathbb{Q}$ and let $R_{+}$ be the positive terms of $R$ .~~

In set theory

~~Let~~ A ~~$S$~~ Cauchy approximation be in a ~~$R_{+}$~~ -premetric space . We ~~define~~ ~~the~~ ~~predicate~~ $S$ is a function $x \in S^{\mathbb{Q}_{+}}$ , where $S^{\mathbb{Q}_{+}}$ is the set of functions with domain $\mathbb{Q}_{+}$ and codomain $S$ , such that

isCauchyApproximation \forall (δ \in ℚ_{+} . \forall η \in ℚ_{+} . x (δ) ≔ \prod_{δ : R_{+}} \prod_{η : R_{+}} x_{δ} \sim_{δ + η} x_{η} x (η)

~~isCauchyApproximation(x)~~ \forall ~~\coloneqq~~ \delta ~~\prod_{\delta:R_{+}}~~ \in ~~\prod_{\eta:R_{+}}~~ \mathbb{Q}_{+}.\forall ~~x_\delta~~ \eta \in \mathbb{Q}_{+}.x(\delta) \sim_{\delta + \eta} ~~x_\eta~~ x(\eta)

~~$x$~~ The set of all Cauchy approximations is defined as ~~is a~~ ~~$R_{+}$ -Cauchy approximation~~ if

x C : R_{+} \to S ⊢ c (x S) : ≔ isCauchyApproximation {x \in S^{ℚ_{+}} | \forall δ \in ℚ_{+} . \forall η \in ℚ_{+} . x (δ) \sim_{δ + η} x (η)}

~~x:R_{+}~~ C(S) ~~\to~~ \coloneqq S \{x ~~\vdash~~ \in ~~c(x):~~ S^{\mathbb{Q}_{+}} ~~isCauchyApproximation(x)~~ \vert \forall \delta \in \mathbb{Q}_{+}.\forall \eta \in \mathbb{Q}_{+}.x(\delta) \sim_{\delta + \eta} x(\eta)\}

~~The type of $R_{+}$ -Cauchy approximations in $S$ is defined as~~

In homotopy type theory

~~$C(S, R_{+}) \coloneqq \sum_{x:R_{+} \to S} isCauchyApproximation(x)$~~

Let $R$ be a dense integral subdomain of the rational numbers $\mathbb{Q}$ and let $R_{+}$ be the positive terms of $R$ .

Let $S$ be a $R_{+}$ -premetric space. We define the predicate

isCauchyApproximation(x) \coloneqq \prod_{\delta:R_{+}} \prod_{\eta:R_{+}} x_\delta \sim_{\delta + \eta} x_\eta

$x$ is a $R_{+}$ -Cauchy approximation if

x:R_{+} \to S \vdash c(x): isCauchyApproximation(x)

The type of $R_{+}$ -Cauchy approximations in $S$ is defined as

C(S, R_{+}) \coloneqq \sum_{x:R_{+} \to S} isCauchyApproximation(x)

Properties

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

Thus, there is a family of dependent terms

x:R_{+} \to S \vdash n(x): isCauchyApproximation(x) \to isCauchyNet(x)

An $R_{+}$ -Cauchy approximation is the composition $x \circ M$ of a net $x$ and an $R_{+}$ -modulus of Cauchy convergence $M$ .

References

Auke B. Booij, Analysis in univalent type theory (pdf)
Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)

Revision on April 13, 2022 at 22:00:18 by Anonymous?. See the history of this page for a list of all contributions to it.