Homotopy Type Theory divisible group > history (Rev #6)

Definition

An abelian group $G$ is a divisible group if there exists a multiplicative $\mathbb{Z}_{+}$-action $\alpha:\mathbb{Z}_{+} \to (G \to G)$, where $\mathbb{Z}_{+}$ is the positive integers, such that for all $n:\mathbb{Z}_{+}$ and all $g:G$, the fiber of $\alpha(n)$ at $g$ is contractible:

$\prod_{n:\mathbb{Z}_{+}} \prod_{g:G} \mathrm{isContr}(\mathrm{fiber}(\alpha(n),g))$