[[!redirects decidable setoids]] ## Contents ## * table of contents {:toc} ## Definition ## A **decidable setoid** is a type $T$ with a function $(-) \equiv (-):T \times T \to \mathbb{2}$ and terms $$r: \prod_{a:A} (a \equiv a) = 1$$ $$s: \prod_{a:A} \prod_{b:A} ((a \equiv b) \implies (b \equiv a)) = 1$$ $$t: \prod_{a:A} \prod_{b:A} \prod_{c:A} ((a \equiv b) \wedge (b \equiv c) \implies (a \equiv c)) = 1$$ A **decidable set** is a decidable setoid where the canonical dependent functions $$idtoequiv(a, b):(a = b) \to ((a \equiv b) = 1)$$ are [[equivalence]]s. ## See also ## * [[decidable set]] * [[decidable directed graph]] * [[booleans]] * [[decidable universal quantifier]] * [[decidable existential quantifier]] category: not redirected to nlab yet