Homotopy Type Theory preorder > history (Rev #5, changes)

Showing changes from revision #4 to #5: Added | Removed | Changed



A preorder on a type TT is a type family ()()(-)\leq(-) over TT with

  • a family of dependent terms

    a:T,b:Tπ(a,b):isProp(ab)a:T, b:T \vdash \pi(a,b):isProp(a \leq b)

    representing that each type aba \leq b is a proposition.

  • a family of dependent terms

    a:Tρ(a):aaa:T \vdash \rho(a):a \leq a

    representing the reflexive property of \leq.

  • a family of dependent terms

    a:T,b:T,c:Tτ(a,b,c):(ab)×(bc)(ac)a:T, b:T, c:T \vdash \tau(a, b, c):(a \leq b) \times (b \leq c) \to (a \leq c)

    representing the transitive property of \leq.

If TT comes with a preorder, then TT is a preordered type or a (0,1)-precategory.


Every preordered type in a univalent universe is a set and a poset.

See also


Revision on April 27, 2022 at 11:22:18 by Anonymous?. See the history of this page for a list of all contributions to it.