Homotopy Type Theory set > history (Rev #6)

Contents

Definition

A set consists of

• A type $A$
• A 0-truncator
  $$\tau_0: \prod_{(a:A)} \prod_{(b:A)} \mathrm{isProp}(a = b)$$

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