done new exercise 5.6.4

actions.tex

@@ -1550,18 +1550,18 @@ \section{Any symmetry is a symmetry in $\Set$}
 equal as pointed maps.
 \end{xca}
 
-\begin{remark}\label{rem:CayleyMaybeLarge}
+\begin{remark}\label{rem:CayleyOversize}
 \MB{New:} In many cases, the set $\USymG$ used in \cref{lem:allgpsarepermutationgps} is larger than necessary for
-obtaining the symmetries in $G$ as symmetries of the set.
+obtaining the symmetries in $G$ as symmetries of a set.
 A case in point is the group $\SG_3$, where the symmetries \emph{are}
 already symmetries of a set, namely of the set $\bn3$. However,
 $\USG_3\jdeq(\bn3\eqto\bn3)$ is a $6$-element set. 
 Let's take a closer look at where and how this happens in the proof.
 
-As shown in \cref{xca:evP_isPrG}, the map $\princ G: 
+As stated in \cref{xca:evP_isPrG}, the map $\princ G: 
 \BG\ptdto\conncomp{\Set}{\USymG}$ classifying the monomorphism $\rho_G$ 
 is decomposed as an equivalence $\pathsp{\blank}$
-followed by a map $\ev_{\sh_G}$ classifying a monomorphism.
+followed by the evaluation map $\ev_{\sh_G}$.
 This is depicted in the following diagram, where the
 second line shows the induced maps on the symmetries.
    \[
@@ -1582,25 +1582,32 @@ \section{Any symmetry is a symmetry in $\Set$}
 By \cref{lem:fixpts-are-fixed}\ref{it:ev-is-inj}, such fixed points,
 and hence the corresponding symmetries of $\princ G$, are uniquely
 determined by their value at $\sh_G$.\footnote{%
-This is an alternative way to understand that $\ev_{\sh_G}$ classifies
-a monomorphism.}
+This is an alternative way to understand that $\ev_{\sh_G}$,
+and hence $\princ G$, classifies a monomorphism.}
 
 Note that the underlying set of $\PP$ is 
 $\PP(\sh_G)\jdeq(\USymG \eqto \USymG)$.
 However, $\PP$ has more structure than its underlying set.
-\cref{lem:fixpts-are-fixed}\ref{it:ev-is-eq-on-inv} tell us
-exactly which fixed points of $\PP$ we get, namely those
-corresponding with invariant elements of $\USymG \eqto \USymG$.
-
-Finally, $\ev_{\sh_G}$ forgets about the extra structure of $\PP$
+\cref{lem:fixpts-are-fixed}\ref{it:ev-is-eq-on-inv} characterizes
+exactly the fixed points of $\PP$ as corresponding via $\ev_{\sh_G}$
+with invariant elements of $\USymG \eqto \USymG$. In other words,
+$\ev_{\sh_G}$ forgets about the extra structure of $\PP$
 and maps fixed points of $\PP$ to invariant permutations of $\USymG$.
 For example, in the case of $\SG_3$, we go in total from permutations
-of $\bn3$ to invariant permutations the $6$-element set $\bn3\eqto\bn3$.
-In \cref{xca:invariant-permutations} you are asked ...
-\end{remark}
+of $\bn3$ to invariant permutations of the $6$-element set $\bn3\eqto\bn3$.
 
-\begin{xca}\label{xca:invariant-permutations} \MB{New:}
+In \cref{xca:PP-invariant-permutations} you are asked to explore
+the abstract group of invariant permutations of $\USymG$.
+\end{remark}
 
+\begin{xca}\label{xca:PP-invariant-permutations} \MB{New:}
+Let conditions be as in \cref{rem:CayleyOversize}.
+By analyzing transport in the type family $\princ G(\blank)$,
+show that a permutation $\pi$ of $\USymG$
+is invariant if and only if $\pi(gg')=g\pi(g')$ for all $g,g':\USymG$.
+Show that the invariant permutations of $\USymG$ form an abstract group
+and that evaluation of such a permutation at $\refl{\sh_G}$
+yields an abstract isomorphism from this group to $\abstr(G)$.
 \end{xca}