Homotopy Type Theory set > history (Rev #5)

Contents

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$$

As univalent setoids

A set is a setoid $T$ where the canonical functions

are equivalences

Examples

• A monoid is a set that is also an A3-space.

See also

• contractible type

• proposition

• groupoid

• homotopy level

• setoid

References

• HoTT book