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)