Showing changes from revision #5 to #6:
Added | Removed | Changed
A preorder on a type is a type family over with
a family of dependent terms
representing that each type is a proposition.
a family of dependent terms
representing the reflexive property of .
a family of dependent terms
representing the transitive property of .
If comes with a preorder, then is a preordered type or a (0,1)-precategory.
Every preordered type in a univalent universe is a set and a poset.
Benedikt Ahrens, Paige Randall North, Michael Shulman, Dimitris Tsementzis, The Univalence Principle (abs:2102.06275)
Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)
Last revised on June 10, 2022 at 17:07:14. See the history of this page for a list of all contributions to it.