Homotopy Type Theory
premetric space > history (Rev #4, changes)
Showing changes from revision #3 to #4:
Added | Removed | Changed
Definition
Let be a Archimedean ordered integral domain with a dense linear order?dense , and letstrict order , be and the let be the semiring? of positive terms in . 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 March 11, 2022 at 20:59:10 by
Anonymous?.
See the history of this page for a list of all contributions to it.