A preorder on a type $T$ is a type family $(-)\leq(-)$ over $T$ with
a family of dependent terms
representing that each type $a \leq b$ is a proposition.
a family of dependent terms
representing the reflexive property of $\leq$.
a family of dependent terms
representing the transitive property of $\leq$.
If $T$ comes with a preorder, then $T$ 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)