wip up to 4.3.7

group.tex

@@ -705,7 +705,7 @@ \subsection{First examples}
 \begin{remark}
 In \cref{lem:idtypesgiveabstractgroups} we will see that the identity type
 of a group satisfies a list of laws justifying the name ``group'' and
-we will later show in \cref{thm:Groupsareidentitytypes} that groups
+we will later show in \cref{lem:Groupsareidentitytypes} that groups
 are uniquely characterized by these laws.
 \end{remark}
 Some groups have the property that the order you compose the 
@@ -782,7 +782,8 @@ \subsection{First examples}
 \section{Abstract groups}
 \label{sec:identity-type-as-abstract}
 
-Studying the identity type leads one to the definition of what an abstract group should be.  We fix a type $A$ and an element $a:A$ for the rest
+Studying the identity type leads one to the definition of what an 
+abstract group should be. We fix a type $A$ and an element $a:A$ for the rest
 of the section, and we focus on the identity type $a\eqto a$.
 We make the following observations about its elements and operations on them.
 
@@ -799,7 +800,8 @@ \section{Abstract groups}
   Because it was defined by path induction, this product operation satisfies $e \cdot g \jdeq g$.
 \end{enumerate}
 
-For any elements $g,g_1,g_2,g_3:a\eqto a$, we consider the following four equations:
+For any elements $g,g_1,g_2,g_3:a\eqto a$, we consider the 
+following four identity types:
 \begin{enumerate}
 \item
   \label{it:right-unit} \emph{the right unit law:} $g \eqto g\cdot e$,
@@ -812,20 +814,26 @@ \section{Abstract groups}
   \label{it:inverse} \emph{the law of inverses:} $g\cdot \inv g \eqto e$.
 \end{enumerate}
 
-In \cref{xca:path-groupoid-laws}, the reader has constructed explicit elements of these equations.  If $a\eqto a$ were a set, then the equations
-above would all be propositions, and then, in line with the convention adopted in \cref{sec:props-sets-grpds}, we could simply say that
-\cref{xca:path-groupoid-laws} establishes that the equations hold.  That motivates the following definition, in which we introduce a new set $S$
-to play the role of $a\eqto a$.
-We introduce a new element $e:S$ to play the role of $\refl a$, a new multiplication operation, and a new inverse
-operation.  The original type $A$ and its element $a$ play no further role.
+In \cref{xca:path-groupoid-laws}, the reader has constructed explicit
+elements of these identity types. 
+If $a\eqto a$ is a set, then the identity types
+above are all propositions. Then, in line with the convention adopted 
+in \cref{sec:props-sets-grpds}, we could simply say that
+\cref{xca:path-groupoid-laws} establishes that the equations hold.
+That motivates the following definition, 
+in which we introduce a new set $S$ to play the role of $a\eqto a$.
+We introduce a new element $e:S$ to play the role of $\refl a$, 
+a new multiplication operation, and a new inverse operation. 
+The original type $A$ and its element $a$ play no further role.\footnote{%
+In \cref{sec:inftygps} we will come back to $A$ and $a$ and
+consider the case in which $A$ is an arbitrary connected type
+and $a:A$. Then $a\eqto a$ need not be a set.}
 
 \begin{definition}\label{def:abstractgroup}
   An \emph{abstract group}\index{abstract group}\index{group!abstract}
   consists of the following data.
   \begin{enumerate}
-  \item\label{struc:under-set} A type $S$.
-    \par \noindent
-    Moreover, the type $S$ should be a set.  It is called the \emph{underlying set}.
+  \item\label{struc:under-set} A set $S$, called the \emph{underlying set}.
   \item\label{struc:unit} An element $e:S$, called the \emph{unit} or the \emph{neutral element}.\index{neutral element}
   \item\label{struc:mult-op} A function $S\to S\to S$, called \emph{multiplication},
     taking two elements $g_1,g_2:S$ to their \emph{product}, denoted by $g_1\cdot g_2:S$.
@@ -861,7 +869,8 @@ \section{Abstract groups}
 Taking into account the introductory comments we have made above, we may state the following lemma.
 
 \begin{lemma}\label{lem:idtypesgiveabstractgroups}
-  If $G$ is a group, then $\USymG$,
+  If $G$ is a group, then the set $\USymG \jdeq (\sh_G\eqto\sh_G)$
+  of symmetries in $G$ (see \cref{def:group-symmetries}),
   together with $e\defequi\refl{\shape_G}{}$,
   $g^{-1}\defequi\symm_{\shape_G,\shape_G}g$
   and $h \cdot g \defequi \trans_{\shape_G,\shape_G,\shape_G}(g)(h)$, define an abstract group.