# Homotopy Type Theory infinity-group > history (Rev #1)

## Definition

An $\infty$-group or pointed connected type 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})$

## References

Revision on May 1, 2022 at 22:59:30 by Anonymous?. See the history of this page for a list of all contributions to it.