Homotopy Type Theory groupoid > history (Rev #1)

Contents

Definition

A groupoid consists of

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

See also

References

Revision on May 1, 2022 at 21:41:02 by Anonymous?. See the history of this page for a list of all contributions to it.