Homotopy Type Theory premetric space > history (Rev #8, changes)

Showing changes from revision #7 to #8: Added | ~~Removed~~ | ~~Chan~~ged

Definition
- In set theory
- In homotopy type theory
Examples
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

A ~~$R_{+}$~~ premetric space~~-premetric space~~ is a ~~type~~ set $S$ with a ~~family~~ ternary of relation ~~types~~ $\sim$ on the Cartesian product $\mathbb{Q}_{+} \times S \times S$ , where

a ℚ_{+} : ≔ S {, x b \in : ℚ S |, 0 ϵ < : x R_{+}} ⊢ a \sim_{ϵ} b type

~~a:S,~~ \mathbb{Q}_{+} ~~b:S,~~ \coloneqq ~~\epsilon:R_{+}~~ \{x ~~\vdash~~ \in a \mathbb{Q} ~~\sim_{\epsilon}~~ \vert b 0 \ \lt ~~type~~ x\}

~~called~~ is the set of positive rational numbers. ~~$R_{+}$ -premetric, and a family of dependent terms~~

~~$a:S, b:S, \epsilon:R_{+} \vdash p(a, b, \epsilon):isProp(a \sim_{\epsilon} b)$~~

In homotopy type theory

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

A $R_{+}$ -premetric space is a type $S$ with a family of types

a:S, b:S, \epsilon:R_{+} \vdash a \sim_{\epsilon} b \ type

called the $R_{+}$ -premetric, and a family of dependent terms

a:S, b:S, \epsilon:R_{+} \vdash p(a, b, \epsilon):isProp(a \sim_{\epsilon} b)

representing that the $R_{+}$ -premetric is a predicate.

Examples

A $\mathbb{Q}_{+}$ -premetric on $\mathbb{R}_H$ is used to define the HoTT book real numbers.

References

Auke B. Booij, Analysis in univalent type theory (pdf)

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