## Definition A **set** is a 0-[[truncated]] [[type]]. ## References * [[HoTT book]]