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

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

Definition

Given a decidable set (A,)(A, \equiv), a function ()<():A×A𝟚(-)\lt(-):A \times A \to \mathbb{2} is a decidable strict order (also called decidable strict total order, decidable strict linear order, or decidable pseudo-order) if it comes with

  • an identity

    ι: a:AP(a)=1\iota: \prod_{a:A} P(a) = 1

    representing the irreflexivity condition for the decidable binary relation, where the decidable predicate P(a)P(a) is defined as

    P(a)¬(a<a)P(a) \coloneqq \neg(a \lt a)
  • an identity

    κ: a:A b:A c:AQ(a,b,c)=1\kappa: \prod_{a:A} \prod_{b:A} \prod_{c:A} Q(a,b,c) = 1

    representing the comparison condition for the binary relation, where the decidable predicate Q(a,b,c)Q(a,b,c) is defined as

    Q(a,b,c)(a<c)((a<b)(b<c))Q(a,b,c) \coloneqq (a \lt c) \implies ((a \lt b) \vee (b \lt c))
  • an identity

    γ: a:A b:AR(a,b)=1\gamma: \prod_{a:A} \prod_{b:A} R(a,b) = 1

    representing the connectedness condition for the binary relation, where the decidable predicate R(a,b)R(a,b) is defined as

    R(a,b)¬((a<b)(b<a))(ab)R(a,b) \coloneqq \neg((a \lt b) \wedge (b \lt a)) \implies (a \equiv b)
  • an identity

    α: a:A b:AS(a,b)=1\alpha: \prod_{a:A} \prod_{b:A} S(a,b) = 1

    representing the asymmetry condition for the binary relation, where the decidable predicate S(a,b)S(a,b) is defined as

    S(a,b)(a<b)¬(b<a)S(a,b) \coloneqq (a \lt b) \implies \neg(b \lt a)

AA is called a decidable strictly ordered set.

See also

Revision on June 18, 2022 at 21:49:32 by Anonymous?. See the history of this page for a list of all contributions to it.