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

Showing changes from revision #1 to #2: Added | ~~Removed~~ | ~~Chan~~ged

Definition

Given a decidable ~~setoid~~ set $(A, \equiv)$ , ~~with~~ a function~~decidable universal quantifier~~ $(-)\lt(-):A \times A \to \mathbb{2}$ s is adecidable strict order (also called decidable strict total order, decidable strict linear order, or decidable pseudo-order) if it comes with

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

an identity

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

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

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

$\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)$ is defined as

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

$\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)$ is defined as

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

$\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)$ is defined as

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

~~$\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$ is called a decidable strictly ordered set.

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 #2, changes)

Definition

See also