[[!redirects groupoids]] ## Contents ## * table of contents {:toc} ## 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]]