Showing changes from revision #2 to #3:
Added | ~~Removed~~ | ~~Chan~~ged

A **groupoid** consists of

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

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