[[!redirects sets]] [[!redirects univalent setoid]] ## Contents ## * table of contents {:toc} ## Definition A __set__ consists of * A [[type]] $A$ * A set-truncator $$\tau_0: \prod_{a:A} \prod_{b:A} \prod_{c:(a = b)} \prod_{d:(a = b)} c = d$$ ## See also * [[proposition]] category: not redirected to nlab yet