## Definition A __set__ consists of * A [[type]] $A$ * A 0-truncator $$\tau_0: \prod_{(a:A)} \prod_{(b:A)} \prod_{(c:a=b)} \prod_{(d:a=b)} \sum_{(x:c=d)} \prod_{(y:c=d)} x=y$$ ## Examples * A [[monoid]] is a [[set]] that is also an [[A3-space]]. ## See also * [[contractible type]] * [[proposition]] * [[groupoid]] * [[homotopy level]] ## References * [[HoTT book]]