Homotopy Type Theory groupoid > history (changes)

Showing changes from revision #2 to #3: Added | Removed | Changed

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

Last revised on June 15, 2022 at 18:19:11. See the history of this page for a list of all contributions to it.