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

Showing changes from revision #8 to #9: 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 on it a comes type withAA is a type family on A×AA \times A with

  • a family of dependent terms

    a:A,b:A ι π(a,b):( c:(a<b)a d:(a<b)<ca=)d a:A a:A, b:A \vdash \iota(a): \pi(a, (a b): \prod_{c:(a \lt a) b)} \to \prod_{d:(a \emptyset \lt b)} c = d

    representing that the irreflexivity dependent condition type for is the a binary proposition relation

  • a family of dependent terms

    a:A,b:A,c:A κ ι(a):(a< c a)[(a<b)+(b<c)] a:A, a:A b:A, c:A \vdash \kappa(a): \iota(a): (a \lt c) a) \to \left[(a \emptyset \lt b) + (b \lt c) \right]

    representing the comparison irreflexivity condition for the binary dependent relation type

  • a family of dependent terms

    a:A,b:A,c:A γ κ(a):((a< b c)[(a<b)+(b<c)])×((b<a))(a=b) a:A, b:A b:A, c:A \vdash \gamma(a): \kappa(a): ((a (a \lt b) c) \to \emptyset) \left[(a \times ((b \lt a) \to \emptyset) \to (a = b) + (b \lt c) \right]

    representing the connectedness comparison condition for the binary dependent relation type

  • a family of dependent terms

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

    representing the asymmetry connectedness condition for the binary dependent relation type

  • 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 dependent type

AA is called a strictly ordered type.

See also

Revision on June 16, 2022 at 02:56:48 by Anonymous?. See the history of this page for a list of all contributions to it.