Homotopy Type Theory set > history (Rev #8)

Contents

Definition

A set consists of

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

See also

• contractible type

• proposition

• homotopy level

References

• HoTT book