Homotopy Type Theory
premetric space > history (Rev #5, changes)
Showing changes from revision #4 to #5:
Added | Removed | Changed
Definition
Let Given a type , be aArchimedean ordered integral domain-premetric space with is a typedense strict order, and 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 12, 2022 at 07:53:35 by
Anonymous?.
See the history of this page for a list of all contributions to it.