[[!redirects decidable sets]] ## Contents ## * table of contents {:toc} ## Definition ## A **decidable set** is a [[decidable setoid]] $(T, (-)\equiv(-): T \times T \to \mathbb{2})$ where the canonical dependent functions $$a:T, b:T \vdash idtoequiv(a, b):(a = b) \to ((a \equiv b) = 1)$$ are [[equivalence]]s. ## See also ## * [[booleans]] * [[set]] * [[limited principle of omniscience]] * [[decidable subset]] * [[decidable setoid]] * [[decidable strict order]] category: not redirected to nlab yet