[[!redirects decidable preordered type]] ## Contents ## * table of contents {:toc} ## Definition ## A **decidable preordered type** is a type $T$ with a function $(-) \leq (-):T \times T \to \mathbb{2}$ and terms $$r: \prod_{a:A} (a \leq a) = 1$$ $$t: \prod_{a:A} \prod_{b:A} \prod_{c:A} ((a \leq b) \wedge (b \leq c) \implies (a \leq c)) = 1$$ ## See also ## * [[decidable directed graph]] * [[decidable setoid]] * [[booleans]] category: not redirected to nlab yet