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

Skip the Navigation Links | Home Page | All Pages | Latest Revisions | Authors |

Showing changes from revision #8 to #9: Added | Removed | Changed

Contents

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

 Definition

In set theory

A Letpremetric spaceℚ\mathbb{Q} is be a the setSSrational numbers with and a let ternary relation∼\sim on the Cartesian product ℚ +×S×S\mathbb{Q}_{+} \times S \times S, where

ℚ +≔{x∈ℚ|0<x}\mathbb{Q}_{+} \coloneqq \{x \in \mathbb{Q} \vert 0 \lt x\}

is be the set of positive rational numbers.

A premetric space is a set SS with a ternary relation ∼\sim on the Cartesian product ℚ +×S×S\mathbb{Q}_{+} \times S \times S.

In homotopy type theory

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

A R +R_{+}-premetric space is a type SS with a family of types

ℚ +≔∑ x:ℚ0<x\mathbb{Q}_{+} \coloneqq \sum_{x:\mathbb{Q}} 0 \lt x
a:S,b:S,ϵ:R +⊢a∼ ϵbtypea:S, b:S, \epsilon:R_{+} \vdash a \sim_{\epsilon} b \ type

be the positive rational numbers.

called A theR +R_{+}premetric space-premetric , and is a family type of dependent termsSS with a family of types

a:S,b:S,ϵ: R ℚ +⊢p(a,b,ϵ):isProp(a∼ ϵb)type a:S, b:S, \epsilon:R_{+} \epsilon:\mathbb{Q}_{+} \vdash p(a, a b, \epsilon):isProp(a \sim_{\epsilon} b) b \ type

representing called that theR +R_{+}premetric -premetric , is and a family of dependent termspredicate.

a:S,b:S,ϵ:ℚ +⊢p(a,b,ϵ):isProp(a∼ ϵb)a:S, b:S, \epsilon:\mathbb{Q}_{+} \vdash p(a, b, \epsilon):isProp(a \sim_{\epsilon} b)

representing that the premetric is a predicate.

Examples

  • A premetric on ℚ ℝ +H \mathbb{Q}_{+} \mathbb{R}_H-premetric on ℝ H\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 April 14, 2022 at 00:16:26 by Anonymous?. See the history of this page for a list of all contributions to it.

DiscussNext revision (2 more)Previous revision (8 more)Current version of pageHide changesHistory (10 revisions)Rollback Source