Homotopy Type Theory set > history (Rev #4)

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