Homotopy Type Theory decidable strict order > history (Rev #1)

Definition

Given a decidable setoid $(A, \equiv)$ with decidable universal quantifiers

\forall a.(-)(a):(A \to \mathbb{2}) \to \mathbb{2}

\forall (a,b).(-)(a,b):(A \times A \to \mathbb{2}) \to \mathbb{2}

\forall (a,b,c).(-)(a,b,c):(A \times A \times A \to \mathbb{2}) \to \mathbb{2}

a function $(-)\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

$\iota: \forall a \in A.P(a) = 1$

representing the irreflexivity condition for the decidable binary relation, where the decidable predicate

$P(a) \coloneqq \neg(a \lt a)$
an identity

$\kappa: \forall (a, b, c).Q(a,b,c) = 1$

representing the comparison condition for the binary relation, where the decidable predicate

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

$\gamma: \forall (a, b).R(a,b) = 1$

representing the connectedness condition for the binary relation, where the decidable predicate

$R(a,b) \coloneqq \neg((a \lt b) \wedge (b \lt a)) \implies (a \equiv b)$
an identity

$\alpha: \forall (a, b).S(a,b) = 1$

representing the asymmetry condition for the binary relation, where the decidable predicate

$S(a,b) \coloneqq (a \lt b) \implies \neg(b \lt a)$

$A$ is called a decidable strictly ordered type.

Homotopy Type Theory decidable strict order > history (Rev #1)

Definition

See also