Homotopy Type Theory strict order > history (Rev #2, changes)

Showing changes from revision #1 to #2: Added | Removed | Changed

Definition

A binary relation <\lt over a type AA is a strict order (also called strict total order, strict linear order, or pseudo-order) if it comes with

  • a family of dependent terms

    a:Aι(a):(a<a)a:A \vdash \iota(a): (a \lt a) \to \emptyset

    representing the irreflexivity condition for the binary relation

  • a family of dependent terms

    a:A,b:A,c:Aκ(a):(a<c)(a<b)+(b<c)a:A, b:A, c:A \vdash \kappa(a): (a \lt c) \to \Vert (a \lt b) + (b \lt c) \Vert

    representing the comparison condition for the binary relation

  • a family of dependent terms

    a:A,b:Aγ(a):((a<b))×((b<a))(a=b)a:A, b:A \vdash \gamma(a): ((a \lt b) \to \emptyset) \times ((b \lt a) \to \emptyset) \to (a = b)

    representing the connectedness condition for the binary relation

  • a family of dependent terms

    a:A,b:Aα(a,b):(a<b)((b<a))a:A, b:A \vdash \alpha(a, b): (a \lt b) \to ((b \lt a) \to \emptyset)

    representing the asymmetry condition for the binary relation

AA is called a strictly ordered type.

See also

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