[[!redirects sets]] [[!redirects univalent setoid]] ## Contents ## * table of contents {:toc} ## Definition A __set__ consists of * A [[type]] $A$ * A 0-truncator $$\tau_0: \prod_{(a:A)} \prod_{(b:A)} \mathrm{isProp}(a = b)$$ ### As univalent setoids A set is a [[setoid]] $T$ where the canonical functions $$a:T, b:T \vdash idtoiso(a,b):(a =_T b) \to (a \equiv b)$$ are [[equivalence]]s $$p: \prod_{a:A} \prod_{b:A} (a =_T b) \cong (a \equiv b)$$ ## Examples * A [[monoid]] is a [[set]] that is also an [[A3-space]]. ## See also * [[contractible type]] * [[proposition]] * [[groupoid]] * [[homotopy level]] * [[setoid]] ## References * [[HoTT book]]