[[!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$$ ## See also ## * [[setoid]] * [[decidable set]] * [[decidable preordered type]] * [[booleans]] * [[decidable universal quantifier]] * [[decidable existential quantifier]]