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

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

Definition

~~Given~~ Let a ~~type~~ $T R$ T R , be a dense integral subdomain of the ~~$T$ -premetric space~~rational numbers is a ~~type~~ $S ℚ$ S \mathbb{Q} ~~with~~ and a let ~~family~~ of ~~types~~ $R_{+}$ be the positive terms of $R$ .

~~$a:S, b:S, \epsilon:T \vdash a \sim_{\epsilon} b \ type$~~

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

~~called the $T$ -premetric, and a family of dependent terms~~

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

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

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

~~representing that the $T$ -premetric is a predicate.~~

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 March 31, 2022 at 03:00:41 by Anonymous?. See the history of this page for a list of all contributions to it.

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

Definition

Examples

See also

References