Rem. 4.2.21 replaced by mn 8

group.tex

@@ -436,33 +436,10 @@ \subsection{First examples}
   so we can also identify the trivial group with
   $\mkgroup (\true,\triv)$, or with $\mkgroup (C,c)$ for
   any contractible type $C$ and element $c:C$, or
-  with $\Aut_{S}(x)$ for any set $S$ and element $x:S$.
-
-  \item\label{ex:permgroup}
-    If $n:\NN$, then the \emph{permutation group of $n$ letters}
-    (also known as the \emph{symmetric group of order $n$}) is%
-    \glossary(918Sigma2){$\protect\SG_n$}{symmetric group of order $n$,
-      \cref{ex:groups}\ref{ex:permgroup}}\index{symmetric group}%
-    \index{group!symmetric group}
-    \[
-      \SG_n\defequi \Aut_{\Set}(\bn n). %\mkgroup(\FinSet_n,\bn{n}),
-    \]
-    The classifying type is thus $\BSG_n\jdeq (\FinSet_n,\bn{n})$,   
-    where $\FinSet_n \jdeq \Set_{(\bn{n})}$ is the groupoid of 
-    sets of cardinality $n$ (\cf \ref{def:groupoidFin}).
-
-    Again, we can also identify the group $\SG_n$ with
-    $\Aut_\FinSet(\bn{n})$ (by \cref{xca:group-example-details}), with 
-    $\Aut_{\FinSet_n}(\bn n)$ (by \cref{rem:symmetriesofnonconnectedgroupoids}),
-    or even with $\Aut_{\UU}(\bn n)$ (by stretching the definition of $\Aut$,
-    using that $\UU_{(\bn n)}$ is a connected groupoid, see~\cref{rem:autinfgp}).
-
-
-    If the reader starts worrying about size issues,
-    see~\cref{rem:groupsarebig}.\footnote{%
-This footnote is for those who worry about size issues -- a
+  with $\Aut_{S}(x)$ for any set $S$ and element $x:S$.\footnote{%
+This note is for those who worry about size issues -- a
 theme we usually ignore in our exposition. 
-Recall from \MB{updated} \cref{sec:universes} the chain of
+Recall from \cref{sec:universes} the chain of
 universes $\UU_0 : \UU_1 : \UU_2 : \dots$ such that for each $i$
 all types in $\UU_i$ are also in $\UU_j$ for all $j>i$.
 Let $\Set_0$ be the type of sets in $\UU_0$, 
@@ -494,9 +471,30 @@ \subsection{First examples}
 However, even with this principle there are groups that only belong
 to $\typegroup_i$ for $i>0$ large enough.
 
-These matters concerning universes are nontrivial and important,
+Issues concerning universes are nontrivial and important,
 but in this text we have chosen to focus on other matters.
 }
+
+  \item\label{ex:permgroup}
+    If $n:\NN$, then the \emph{permutation group of $n$ letters}
+    (also known as the \emph{symmetric group of order $n$}) is%
+    \glossary(918Sigma2){$\protect\SG_n$}{symmetric group of order $n$,
+      \cref{ex:groups}\ref{ex:permgroup}}\index{symmetric group}%
+    \index{group!symmetric group}
+    \[
+      \SG_n\defequi \Aut_{\Set}(\bn n). %\mkgroup(\FinSet_n,\bn{n}),
+    \]
+    The classifying type is thus $\BSG_n\jdeq (\FinSet_n,\bn{n})$,   
+    where $\FinSet_n \jdeq \Set_{(\bn{n})}$ is the groupoid of 
+    sets of cardinality $n$ (\cf \ref{def:groupoidFin}).
+
+    Again, we can also identify the group $\SG_n$ with
+    $\Aut_\FinSet(\bn{n})$ (by \cref{xca:group-example-details}), with 
+    $\Aut_{\FinSet_n}(\bn n)$ (by \cref{rem:symmetriesofnonconnectedgroupoids}),
+    or even with $\Aut_{\UU}(\bn n)$ (by stretching the definition of $\Aut$,
+    using that $\UU_{(\bn n)}$ is a connected groupoid, see~\cref{rem:autinfgp}).
+
+
 
   \item\label{ex:genpermgroup}
     More generally, if $S$ is a set, is there a pointed connected groupoid $(A,a)$ so that $a\eqto_Aa$ models all the ``permutations'' $S\eqto_{\Set}S$ of $S$?
@@ -524,37 +522,6 @@ \subsection{First examples}
   Also, give an identification of type $\Aut_\Set(\NN)\eqto\Aut_\Set(\zet)$. 
 \end{xca}
 
-\begin{remark}
-  \label{rem:groupsarebig}
-  This remark is for those who worry about size issues -- a theme we usually ignore in our exposition.  If we
-  start with a base universe $\UU_0$, the groupoid $\FinSet_n$ of sets of cardinality $n$ is the $\Sigma$-type
-  $\sum_{A:\UU_0}\Trunc{A\eqto\bn{n}}$ over $\UU_0$ and so (without any modification) will lie in any bigger
-  universe $\UU_1$.  In order to accommodate the permutation groups of sets in $\UU_0$, the universe ``$\UU$'' appearing as
-  a subscript of the first $\Sigma$-type in \cref{def:pt-conn-groupoid}, appearing later in the definition of
-  ``group'', needs to be at least as big as $\UU_1$.  If $\UU$ is taken to be $\UU_1$, then the type
-  $\typegroup$ of groups will not be in $\UU_1$, but in some bigger universe $\UU_2$.
-  If we then choose some group $G:\typegroup$
-  and look at its group of automorphisms, $\Aut_\Group(G)$,\footnote{%
-    \Cref{xca:typegroupisgroupoid} below asks you to verify that $\Group$
-    is a (large) groupoid.}
-  based on the identity type $G \eqto_\Group G$, this will be an element of $\typegroup$ only if the universe $\UU$ in the definition of
-  $\typegroup$ is at least as big as $\UU_2$.  Our convention from \cref{sec:universes} is
-  that the universes form an ascending chain $\UU_0\subseteq\UU_1\subseteq\UU_2\subseteq\dots$, corresponding
-  to which there will an ascending chain of types of groups,
-  \[
-    \typegroup_i \defequi \Copy_{\mkgroup}\bigl( (\UU_i)_*^{=1} \bigr) : \UU_{i+1},
-  \]
-  and any group we encounter will be an element of $\typegroup_i$ for $i$
-  large enough.
-
-  These matters concerning universes are nontrivial and important,
-  but in this text we have chosen to focus on other matters.\footnote{%
-    We will note, however, that the Replacement~\cref{pri:replacement}
-    often allows us to conclude that a group $G$ belongs to $\typegroup_0$.
-    This is the case for $\SG_S$, for $S:\Set_0$, and for $\Aut_\Group(G)$,
-    for $G:\Group_0$, as we invite the reader to check.
-    Hint: use \cref{xca:comp-loc-small-ess-small}.}
-\end{remark}
 
 \begin{example}\label{ex:cyclicgroups}
   In \cref{cor:id-m-cycle} we studied the symmetries of the