Homotopy Type Theory
premetric space > history (Rev #10, changes)
Showing changes from revision #9 to #10:
Added | Removed | Changed
Contents
Whenever editing is allowed on the nLab again, this article should be ported over there.
Definition
In set theory
Let be the rational numbers and let
be the set of positive rational numbers.
A premetric space is a set with a ternary relation on the Cartesian product .
In homotopy type theory
Let be the rational numbers and let
be the positive rational numbers.
A premetric space is a type with a family of types
called the premetric, and a family of dependent terms
representing that the premetric is a predicate.
Examples
See also
References
- Auke B. Booij, Analysis in univalent type theory (pdf)
Revision on April 23, 2022 at 04:00:29 by
Anonymous?.
See the history of this page for a list of all contributions to it.