Homotopy Type Theory groupoid > history (Rev #1)

Contents

Definition

A groupoid consists of

• A type $A$
• A 1-truncator
  $$\tau_1: \prod_{(a:A)} \prod_{(b:A)} \mathrm{isSet}(a = b)$$

See also

• contractible type

• proposition

• set

• groupoid enriched in monoids

• 2-groupoid?

• homotopy level

References

• HoTT book