Homotopy Type Theory premetric space > history (Rev #5)

Definition

Given a type $T$ , a $T$ -premetric space is a type $S$ with a family of types

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

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

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

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

Examples

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

See also

References

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

Revision on March 12, 2022 at 07:53:35 by Anonymous?. See the history of this page for a list of all contributions to it.