Homotopy Type Theory preorder > history (changes)

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

Contents

Definition

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.

Properties

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

See also

References

Last revised on June 10, 2022 at 13:07:14. See the history of this page for a list of all contributions to it.