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

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)$

- Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)
- Marc Bezem, Ulrik Buchholtz, Pierre Cagne, Bjørn Ian Dundas, and Daniel R. Grayson, Symmetry book (2021)

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