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

Showing changes from revision #1 to #2: Added | Removed | Changed

 Definition

Let $R$ be a Archimedean ordered integral domain with a dense linear order?, and let $R_{+}$ be the semiring? of positive terms in $R$. A $R_{+}$-premetric space is a type $T{R}_{+}$ T R_{+} with a family of types

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

representing that the $R_{+}$-premetric for $a:\mathrm{<span><del\; class="diffmod">\; T</del><ins\; class="diffmod">\; A</ins></span>}$ a:T a:A, $b:\mathrm{<span><del\; class="diffmod">\; T</del><ins\; class="diffmod">\; A</ins></span>}$ b:T b:A, $\epsilon:R_{+}$ is a proposition.

See also

• Cauchy structure

  Cauchy structure

• Cauchy net

References

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