Homotopy Type Theory strict order > history (Rev #6)

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 \left[(a \lt b) + (b \lt c) \right]

    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 June 10, 2022 at 13:10:25 by Anonymous?. See the history of this page for a list of all contributions to it.