[[!redirects pointed connected groupoids]] ## Definition ## A __pointed connected groupoid__ consists of * A type $G$ * A basepoint $e:G$ * A 0-connector $$\kappa_1:\prod_{f:G \to \mathbb{1}} \prod_{a:\mathbb{1}} \mathrm{isContr}(\left[\mathrm{fiber}(f, a)\right]_{0})$$ * A 1-truncator: $$\tau_2:\mathrm{isGroupoid}(G)$$ ## See also ## * [[group]] * [[groupoid]] ## References ## * Univalent Foundations Project, [[HoTT book|Homotopy Type Theory – Univalent Foundations of Mathematics]] (2013) * Marc Bezem, Ulrik Buchholtz, Pierre Cagne, Bjørn Ian Dundas, and Daniel R. Grayson, [Symmetry book](https://unimath.github.io/SymmetryBook/book.pdf) (2021)