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

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



A partial order 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.

  • a family of dependent terms

    a:T,b:Tσ(a,b):(ab)×(ba)(a=b)a:T, b:T \vdash \sigma(a, b):(a \leq b) \times (b \leq a) \to (a = b)

    representing the anti-symmetric property of \leq.

If TT comes with a partial order, then TT is a partially ordered type. If TT is also a set, then TT 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.

See also


  • 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,

Revision on June 15, 2022 at 22:57:04 by Anonymous?. See the history of this page for a list of all contributions to it.