Showing changes from revision #2 to #3:
Added | Removed | Changed
A partial order 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 .
a family of dependent terms
representing the anti-symmetric property of .
If comes with a partial order, then is a partially ordered type. If is also a set, then is called a partially ordered set or poset. A poset is also a (0,1)-category.
Every partially ordered type in a univalent universe is a poset.
Ayberk Tosun, Formal Topology in Univalent Foundations pdf
Benedikt Ahrens, Paige Randall North, Michael Shulman, Dimitris Tsementzis, The Univalence Principle (abs:2102.06275)
probably the HoT book as well,