diff --git a/actions.tex b/actions.tex
index 86a7ede..19f5445 100644
--- a/actions.tex
+++ b/actions.tex
@@ -1467,7 +1467,7 @@ \subsection{Homomorphisms and torsors}
    f^*\,\pathsp{\blank}^H$,
    all represented by the following diagram:\footnote{%
    \MB{(MB) Ugly: $f_*$ has no $B$, while $\Bf$ has. 
-   I would like to define $\text{Tors}_G \defeq \Aut_{G-\Set}(\princ G)$
+   I would like to define $\text{Tors}_G \defeq \Aut_{\GSet}(\princ G)$
    so that we can use $\text{BTors}_G$. Further,
    all pointed maps without $B$, and apply $\mkgroup$
    to lift the diagram to groups and iso/homomorphisms.
@@ -1536,23 +1536,39 @@ \section{Any symmetry is a symmetry in $\Set$}
 
 \begin{theorem}[Cayley]
   \label{lem:allgpsarepermutationgps}
-  \marginnote{By \cref{lem:eq-mono-cover} ``$\rho_G$ is a monomorphism'' means that the induced map $\rho_G^\abstr$ from the symmetries of $\shape_G$ in $\BG_\div$ to the symmetries of $\USymG$ in $\Set$ is an injection, \ie ``any symmetry is a symmetry in $\Set$''.}Let $G$ be a group. Then
-  $\rho_G:\Hom(G,\SG_{\USymG})  $ is a monomorphism.
+  \marginnote{By \cref{def:typeofmono}, $\rho_G$ is a monomorphism means 
+  that the induced map $\USym\rho_G$ from the symmetries of $\shape_G$ in 
+  $\BG_\div$ to the symmetries of $\USymG$ in $\Set$ is an injection, 
+  \ie ``any symmetry is a symmetry in $\Set$''.}
+  Let $G$ be a group. Then
+  $(G,\rho_G,!)$ is a monomorphism into $\SG_{\USymG}$.
+  In other words, $G$ is a subgroup of $\SG_{\USymG}$.
 \end{theorem}
 \begin{proof}
-  In view of \cref{lem:eq-mono-cover} we need to show that $\rho_G:\BG\to \conncomp \Set {\USymG}$ is a
-  \covering.
-  Under the identity
-  $$\bar{\pathsp{}}:\BG=(\typetorsor_G,\princ G)$$ of
-  \cref{lem:BGbytorsor}, $\rho_G$ translates to the
+  In view of \cref{def:typeofmono} we need to show that 
+  $\B\rho_G\jdeq\princ G :\BG \to \conncomp \Set {\USymG}$ is a \covering.\footnote{\MB{Confusing, since families of sets are also called \coverings! Better: The fibers of $\princ G$ are sets.}}
+  Under the pointed equivalence
+  $$\pathsp{\blank}:\BG\ptdto (\typetorsor_G,\princ G)$$ of
+  \cref{lem:BGbytorsor}, $\princ G$ translates\footnote{
+  \MB{Exercise? $\princ G(\inv{\pathsp{\blank}}(E)\eqto\ev_{\sh_G}(E)$ for all $E$. Maps pointed, OK for $\sh_G$.}} to the
   evaluation map
-  $$\mathrm{ev}_{\shape_G}:\conncomp{(\BG\to\Set)}{\princ G}\to\conncomp{\Set}{\USymG},\qquad
-  \mathrm{ev}_{\shape_G}(E)=E(\shape_G).$$
+  $$\mathrm{ev}_{\shape_G}:\conncomp{(\BG\to\Set)}{\princ G}\ptdto
+  \conncomp{\Set}{\USymG},\qquad
+  \mathrm{ev}_{\shape_G}(E)\defeq E(\shape_G).$$
   We must show that the preimages
   $\inv{\ev_{\shape_G}}(X)$ for $X:\Sigma_{\USymG}$ are sets.  This
   fiber is equivalent to
-  $\sum_{E:\conncomp{(\BG\to\Set)}{\uc{\sh_G}}}(X=E(\shape_G))$ which is a
-  set precisely when $\sum_{E:\BG\to\Set}(X=E(\shape_G))$ is a set.  We
+  $\sum_{E:\conncomp{(\BG\to\Set)}{\uc{\sh_G}}}(X\eqto E(\shape_G))$ which,
+  \MB{being a subtype}, is a
+  set precisely when $\sum_{E:\BG\to\Set}(X\eqto E(\shape_G))$ is a set.
+  \MB{The latter is the type of pointed maps from $\BG$ to $(\Set,X)$
+  and hence a set by \cref{lem:hom-is-set}, in particular
+  \cref{ft:ptd-decr-h-lev}.}\footnote{%
+  \MB{Rest of the proof not needed. It is not a coincidence that
+  the type is $\Hom(G,\Aut_\Set(X))$, but why exactly? Worth a footnote!}}
+  
+  
+    We
   must then show that if $(E,p),(F,q):\sum_{E:\BG\to\Set}(X=E(\shape_G))$,
   then the type $(E,p)=(F,q)$, which is equivalent
   \marginnote{Note that if $r:\shape_G=x$, then
@@ -1575,13 +1591,13 @@ \section{Any symmetry is a symmetry in $\Set$}
   composite of the identities $\phi(x)=F(r)qp^{-1}E(r)^{-1}=\psi(x)$
   given above.  Since $\BG$ is connected, and $\phi(x)=\psi(x)$ is a
   proposition, one can consider that $\shape_G=x$ is not empty, and we
-  are done.
+  are done.\footnote{\MB{5.6 would become half a page now, a bit short.}}
 \end{proof}
 
 \begin{xca}
     Given a group $G$ we defined in \cref{sec:groupssubperm} a monomorphism from $G$ to the permutation group $\Aut_{\USymG}(\Set)$. Write out the corresponding subgroup of $\Aut_{\USymG}(\Set)$.
   \end{xca}
-  
+
     
 
 \section{The orbit-stabilizer theorem}
diff --git a/group.tex b/group.tex
index ab7a247..9819e30 100644
--- a/group.tex
+++ b/group.tex
@@ -1090,6 +1090,7 @@ \section{Homomorphisms}
   \end{displaymath}
   This concludes the proof that $f\eqto f'$ is a proposition, or in other
   words that $\Hom(G,H)$ is a set.\footnote{%
+    \label{ft:ptd-decr-h-lev}
     The same argument shows that the type $X\ptdto Y$ is a set
     whenever $X$ is connected and $Y$ is a groupoid.
     A more general fact is that $X \ptdto Y$ is an $n$-type