wip 4.6

group.tex

@@ -1958,20 +1958,23 @@ \section{The sign homomorphism}
   (and thus the sign) is preserved, as seen in~\cref{fig:permutation-crossings-isotopy}.
 \end{remark}
 
-\section{\texorpdfstring{\inftygps}{∞-groups}}
+\section{Infinity groups (\texorpdfstring{\inftygps}{∞-groups})}
 \label{sec:inftygps}
 
-Disregarding the set-condition we get the simpler notion of \inftygps:
+Disregarding the requirement that the classifying type
+of a group $G$ is a groupoid (so that $\USym G$ is a set)
+we get the simpler notion of \inftygps:
 \begin{definition}\label{def:inftygps}
   The type of $\infty$-groups is
   \[
     \typeinftygp\defequi \Copy(\UUpconn),
     \quad\text{where}\quad
-    \UUpconn\defeq \sum_{A:\UU}\sum_{a:A} \isconn(A)
+    \UUpconn\defeq \sum_{A:\UU} A\times \isconn(A)
   \]
   is the type of pointed, connected types.
 
-  As for groups, we have the constructor $\mkgroup : \UUpconn \to \typeinftygp$
+  As for groups, we have the constructor 
+  $\mkgroup : \UUpconn \to \typeinftygp$
   and the destructor $\clf : \typeinftygp \to \UUpconn$.
 \end{definition}
 
@@ -2010,8 +2013,8 @@ \section{\texorpdfstring{\inftygps}{∞-groups}}
   Then $\conncomp\UU S$ is a groupoid, and the automorphism $\infty$-group
   $\Aut_\UU(S)$ is an ordinary group.
 
-  Because we have an embedding $\UUp^{=1} \hookrightarrow \UUp^{>0}$,
-  we get a corresponding embedding $\Group \hookrightarrow \typeinftygp$.
+  Because we have an inclusion $\UUp^{=1} \hookrightarrow \UUp^{>0}$,
+  we get a corresponding inclusion $\Group \hookrightarrow \typeinftygp$.
 \end{remark}
 
 \begin{definition}