Set (HoTT)

Definition

Set is homotopy level 0. It refers to the type in which the identity type of any two elements is propositional. In other words, equality is a predicate, meaning that there is no higher structure beyond identity between elements. For a type $X$,

$$\mathrm{isSet}\mathrm{X}⟺\mathrm{\Pi }\mathrm{x},\mathrm{y}:X.\mathrm{\Pi }\mathrm{p},\mathrm{q}:\mathrm{x}=y.\mathrm{p}=\mathrm{q}$$

See also

Contractibility Proposition (HoTT) Homotopy Level Truncation (HoTT)