From 0a1d404426cc8b9378cedd854864a9499c4c910e Mon Sep 17 00:00:00 2001
From: marcbezem <marc.bezem@uib.com>
Date: Thu, 15 Aug 2024 12:14:57 +0200
Subject: [PATCH] wip 4.6

---
 group.tex | 15 +++++++++------
 1 file changed, 9 insertions(+), 6 deletions(-)

diff --git a/group.tex b/group.tex
index 10cd899..04f5440 100644
--- a/group.tex
+++ b/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}