reformulate Lem. 4.11.5 slightly to avoid implicit use of choice

group.tex

@@ -2681,14 +2681,13 @@ \section{Monomorphisms and epimorphisms}
   \footcitetext{TrimbleEpisSurjective}
 \end{lemma}
 \begin{proof}[Proof draft.] Consider the projection $\pi : G \to G/H$ to the set of cosets.
-  Let $j : G/H \to A$ be an injection into an abelian group.
-  (We could for instance let $A$ be the free abelian group on $G/H$. [Add xref to statement that inclusion of generators in an injection.])
+  Let $j : G/H \to A$ be an injection into a group $A$.
+  (We could for instance let $A$ be the free (abelian) group on $G/H$. [Add xref to statement that inclusion of generators in an injection.])
 
-  Consider the group
+  Consider the group $W \defeq \Aut_E(\sh_G,\cst{\sh_A})$, where
   \[
-    W \defeq \mkgroup \sum_{t : \BG}\bigl((\sh_G \eqto t) \to \BA\bigr),
+    E \defeq \sum_{t : \BG}\bigl((\sh_G \eqto t) \to \BA\bigr).
   \]
-  with base point $(\sh_G,\cst{\sh_A})$.
   We have two homomorphisms $\varphi,\psi : G \to W$ with the same underlying map,
   $t \mapsto (t , \cst{\sh_A})$, but with different pointing paths:
   \[