[[!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)$$ ## See also * [[contractible type]] * [[proposition]] * [[homotopy level]] ## References * [[HoTT book]] category: not redirected to nlab yet