diff --git a/fingp.tex b/fingp.tex
index 5497544..6e6d933 100644
--- a/fingp.tex
+++ b/fingp.tex
@@ -11,16 +11,16 @@ \chapter{Finite groups}
  The orbit-stabilizer theorem \cref{sec:orbit-stabilizer-theorem} is at the basis of this analysis: if $G$ is a group and $X:\BG\to\Set$ is a $G$-set, then
 $$X(\shape_G)\simeq \coprod_{x:X/G}\mathcal O_x$$
 and each orbit set $\mathcal O_x$ is equivalent to the cokernel of the inclusion $G_x\subseteq G$ of the stabilizer subgroup of $x$.
-Consequently, if $X(\shape_G)$ is a finite set, then its cardinality is the sum of the cardinality of these cokernels.  If also the set $\USym G$ is finite much more can be said and simple arithmetical considerations often allow us to deduce deep statements like the size of a certain subset of $X(\shape_G)$ and in particular whether or not there are any fixed points.
+Consequently, if $X(\shape_G)$ is a finite set, then its cardinality is the sum of the cardinality of these cokernels.  If also the set $\USymG$ is finite much more can be said and simple arithmetical considerations often allow us to deduce deep statements like the size of a certain subset of $X(\shape_G)$ and in particular whether or not there are any fixed points.
 
 \begin{example}
   A typical application could go like this.
-If $X(\shape_G)$ is a finite set with $13$ elements and for some reason we know that all the orbits have cardinalities dividing $8$ -- which we'll see happens if $\USym G$ has $8$ elements -- then we must have that some orbits are singletons (for a sum of positive integers dividing $8$ to add up to $13$, some of them must be $1$).
+If $X(\shape_G)$ is a finite set with $13$ elements and for some reason we know that all the orbits have cardinalities dividing $8$ -- which we'll see happens if $\USymG$ has $8$ elements -- then we must have that some orbits are singletons (for a sum of positive integers dividing $8$ to add up to $13$, some of them must be $1$).
 That is, $X$ has fixed points.
 \end{example}
 
 The classical theory of finite groups is all about symmetries coupled with simple counting arguments.
-Lagrange's \cref{thm:lagrange} gives the first example: if $H$ is a subgroup of $G$, then the cardinality ``$|G|$'' of $\USym G$ is divisible by $|H|$, putting severe restrictions on the possible subgroups.  For instance, if $|G|$ is a prime number, then $G$ has no nontrivial proper subgroups! (actually, $G$ is necessarily a cyclic group).  To prove this result we interpret $G$ as an $H$-set.
+Lagrange's \cref{thm:lagrange} gives the first example: if $H$ is a subgroup of $G$, then the cardinality ``$|G|$'' of $\USymG$ is divisible by $|H|$, putting severe restrictions on the possible subgroups.  For instance, if $|G|$ is a prime number, then $G$ has no nontrivial proper subgroups! (actually, $G$ is necessarily a cyclic group).  To prove this result we interpret $G$ as an $H$-set.
 
 
 Further examples come from considering the $G$-set $\typesubgroup_G$ of subgroups of $G$ from \cref{sec:subgroups}.  Knowledge about the $G$-set of subgroups is of vital importance for many applications and Sylow's theorems in  \cref{sec:sylow} give the first restriction on what subgroups are possible and how they can interact.  The first step is Cauchy's \cref{thm:cauchys} which says that if $|G|$ is divisible by a prime $p$, then $G$ contains a cyclic subgroup of order $p$.  Sylow's theorems goes further, analyzing subgroups that have cardinality powers of $p$, culminating in very detailed and useful information about the structure of the subgroups with cardinality the maximal possible power of $p$.
@@ -54,7 +54,7 @@ \section{Lagrange's theorem, counting version}
 We start our investigation by giving the version of Lagrange's theorem which has to do with counting, but first we pin down some language.
 \begin{definition}
   \label{def:finitegrd}
-A \emph{finite group}\index{finite group} is a group such that the set $\USym G$ is finite.   If $G$ is a finite group, then the \emph{\gporder}\index{\gporder} $|G|$ is the cardinality of the finite set $\USymG$ (\ie $\USymG:\conncomp\FinSet{|G|}$).
+A \emph{finite group}\index{finite group} is a group such that the set $\USymG$ is finite.   If $G$ is a finite group, then the \emph{\gporder}\index{\gporder} $|G|$ is the cardinality of the finite set $\USymG$ (\ie $\USymG:\conncomp\FinSet{|G|}$).
 \end{definition}
 \begin{example}
   The trivial group has \gporder $1$, the cyclic group $C_n$ of order $n$ has \gporder $n$ %(which is good)
@@ -73,7 +73,7 @@ \section{Lagrange's theorem, counting version}
 If $|H|=|G|$, then $H=G$ (as subgroups of $G$).
 \end{lemma}
 \begin{proof}
-  Consider the $H$ action of $H$ on $G$, \ie the $H$-set $i^*G:\BH\to\Set$ with $i^*G(x)\defequi(\shape_G=\Bi(x))$, so that $G/H$ is just another name for the orbits $i^*G/H\defequi \sum_{x:\BH}i^*G(x)$.  Note that composing with the structure identity $p_i:\shape_G=\Bi(\shape_H)$ gives an equivalence $i^*G(\shape_H)\equiv \USym G$, so that $|i^*G(\shape_H)|= |G|$.
+  Consider the $H$ action of $H$ on $G$, \ie the $H$-set $i^*G:\BH\to\Set$ with $i^*G(x)\defequi(\shape_G=\Bi(x))$, so that $G/H$ is just another name for the orbits $i^*G/H\defequi \sum_{x:\BH}i^*G(x)$.  Note that composing with the structure identity $p_i:\shape_G=\Bi(\shape_H)$ gives an equivalence $i^*G(\shape_H)\equiv \USymG$, so that $|i^*G(\shape_H)|= |G|$.
 
   Lagrange's \cref{thm:lagrange} says that $i^*G$ is a free $H$-set \footnote{\cref{thm:lagrange} doesn't say this at present: fix it} and so all orbits $\mathcal O_x$ are equivalent to the $H$-set $\tilde H(x)=(\shape_H=x$).
 Consequently, the equivalence
@@ -134,34 +134,34 @@ \section{Cauchy's theorem}
 Informally, $\B\CG_p$ consists of pairs $(S,j)$, where $S$ is a set of cardinality $p$ and $j:S\eqto S$ is a cyclic permutation in the sense that for $0<k<p$ we have that $j^k$ is not $\refl{}$ while $j^p=\refl{}$.
 % Note also that $j^?:\bn p\to ((S,j)=(S,j))$ given by $j^?(k)=j^k$ is an equivalence (just as for the integers, a symmetry of $(S,j)$, \ie an $f:S=S$ so that $fj=jf$, must be $j^k$ for some $k:\bn p$, and if $k\neq l$, then $j^k\neq j^l$)
 % If $(S,j):BC_p$ let
-% $$A(S,j)\defequi ((S,j)=(S,j)\to \USym G).$$  Since we have an equivalence $j^?:\bn p\to ((S,j)=(S,j))$ we get that $J:A(S,j)\to \prod_{\bn p}\USym G$ given by $J(g)=(g_{j^0},g_{j_1},\dots,g_{j^{p-1}})$ is an equivalence.
+% $$A(S,j)\defequi ((S,j)=(S,j)\to \USymG).$$  Since we have an equivalence $j^?:\bn p\to ((S,j)=(S,j))$ we get that $J:A(S,j)\to \prod_{\bn p}\USymG$ given by $J(g)=(g_{j^0},g_{j_1},\dots,g_{j^{p-1}})$ is an equivalence.
 Given a set $A$, a function $a : \bn p \to A$ is an ordered $p$-tuple of elements of $A$: it suffices to write $a_i$ for $a(i)$ to retrieve the
 usual notations for tuples. Given $(S,j) : \B\CG_p$ however, functions $S \to A$ cannot really be thought the same because $S$ is not
 explicitely enumerated. But as soon as we are given $q : \zet/p \eqto (S,j)$, then functions $S \to A$ are just as good to model ordered
-$p$-tuples of $A$ (just by precomposing with the first projection of $q$). With this in mind, define $\mu_p : (\bn p \to \USym G) \to \USym G$
+$p$-tuples of $A$ (just by precomposing with the first projection of $q$). With this in mind, define $\mu_p : (\bn p \to \USymG) \to \USymG$
 to be the $p$-ary multiplication, meaning $\mu_p (g) \defequi g_0g_1\ldots g_{p-1}$. Then, one can define
-$\mu:\prod_{(S,j):\B\CG_p}(\zet/p \eqto (S,j)) \to (S\to\USym G)\to \USym G$ by $\mu_{(S,j)}(q)(g)\defequi (gq)_{0}\cdot\dots\cdot (gq)_{p-1}$
+$\mu:\prod_{(S,j):\B\CG_p}(\zet/p \eqto (S,j)) \to (S\to\USymG)\to \USymG$ by $\mu_{(S,j)}(q)(g)\defequi (gq)_{0}\cdot\dots\cdot (gq)_{p-1}$
 (where we use $gq$ abusively to denote the composition of $g$ with the equivalence given by applying the first projection to the identification
 $q$). We can now define the $\CG_p$-set $X:\B\CG_p\to\Set$ as:
-$$X(S,j)\defequi\sum_{g:S \to \USym G}\prod_{q : \zet/p \eqto (S,j)}\mu_{(S,j)}(q)(g) = e_G.$$
-% The map from $X(S,j)$ to the $p-1$-fold product of $\USym G$ with itself sending $(g,!)$ to $(g_{j^1},\dots,g_{j^{p-1}})$ is an equivalence ($\mu_{(S,j)}g=e_G$ says exactly that $g_{j^0}$ can be reconstructed as $(g_{j^1}\cdot\dots\cdot g_{j^{p-1}})^{-1}$), so $X(S,j)$ is a set of cardinality $p-1$ times the \gporder of $G$.  In particular, $p$ divides the \gporder of $X(S,j)$.
+$$X(S,j)\defequi\sum_{g:S \to \USymG}\prod_{q : \zet/p \eqto (S,j)}\mu_{(S,j)}(q)(g) = e_G.$$
+% The map from $X(S,j)$ to the $p-1$-fold product of $\USymG$ with itself sending $(g,!)$ to $(g_{j^1},\dots,g_{j^{p-1}})$ is an equivalence ($\mu_{(S,j)}g=e_G$ says exactly that $g_{j^0}$ can be reconstructed as $(g_{j^1}\cdot\dots\cdot g_{j^{p-1}})^{-1}$), so $X(S,j)$ is a set of cardinality $p-1$ times the \gporder of $G$.  In particular, $p$ divides the \gporder of $X(S,j)$.
 
 % Specializing to $(S,j)$ being $\zet/p$ and allowing to index the elements in $A(\zet/p)$ with $i:\bn p$ (instead of the very awkward ``$(\sqrt[p]\id)^i$'' as purism would dictate) we proceed as follows.
 In particular, an element of $X(\zet/p)$ is a tuple $(g_0,\dots,g_{p-1})$ satisfying that $g_{\sigma 0}\dots g_{\sigma (p-1)} = e_G$ for every
 $\sigma : \USym \CG_p$. Note that this is equivalent to the set of tuples $(g_0,\dots,g_{p-1})$ satisfying that $g_{0}\dots g_{(p-1)} =
-e_G$. So, the map $X(\zet/p)\to \USym G^{p-1}$ that send an element $(g_0,\dots,g_{p-1})$ to $(g_1,\dots,g_{p-1})$ is an equivalence (the
+e_G$. So, the map $X(\zet/p)\to \USymG^{p-1}$ that send an element $(g_0,\dots,g_{p-1})$ to $(g_1,\dots,g_{p-1})$ is an equivalence (the
 condition $g_{0}\dots g_{(p-1)} = e_G$ says exactly that we can reconstruct $g_0$ from $(g_1,\dots,g_{p-1})$). In particular, $p$ divides the
 \gporder of $X(\zet/p)$.%
 
 Now, a $\CG_p$-fixed point of $X$, that is an element $f: \prod_{(S,j):\B\CG_p}X(S,j)$, will have $f_{\zet/p}$ being an element
 $(g_0,\dots,g_{p-1})$ of $X(\zet/p)$ that satisfies (in particular) $(g_0,\dots,g_{p-1})=(g_1,\dots,g_{p-1},g_0)$, \ie{} such that
 $g_0=g_1=g_2=\dots=g_{p-1}$. In other words, a fixed point $f$ is such that $f_{\zet/p}: X(\zet/p)$ is of the form $(g,\dots,g)$ where $g$
-satisfies $g^p=e_G$. So, there is a map $\ev : X^{\CG_p} \to \sum_{g:\USym G}g^p=e_G$ simply given by evaluation at $\zet/p$. This map is an
-equivalence. Indeed, each fiber of $\ev$ is already a proposition, and we only need to show that each is inhabited. Given any $g : \USym G$ such
-that $g^p = e_G$, and given $(S,j) : \B\CG_p$, one can consider the constant function $\hat g : S \to \USym G$ given by $\hat g (s) = g$ for all
+satisfies $g^p=e_G$. So, there is a map $\ev : X^{\CG_p} \to \sum_{g:\USymG}g^p=e_G$ simply given by evaluation at $\zet/p$. This map is an
+equivalence. Indeed, each fiber of $\ev$ is already a proposition, and we only need to show that each is inhabited. Given any $g : \USymG$ such
+that $g^p = e_G$, and given $(S,j) : \B\CG_p$, one can consider the constant function $\hat g : S \to \USymG$ given by $\hat g (s) = g$ for all
 $s:S$. Then, for all $q : \zet/p \eqto (S,j)$, $\hat g q$ is the tuple $(g,\dots,g)$, so that we have $(\hat g, !) : X(S,j)$. In other words, we
 just constructed a fixed point of $X$ whose image through $\ev$ is $g$, that is an element of the fiber of $\ev$ at $g$. In particular,
-$X^{\CG_p}$ is not empty as it is equivalent to $\sum_{g:\USym G}g^p=e_G$, which contains at least $e_G$.
+$X^{\CG_p}$ is not empty as it is equivalent to $\sum_{g:\USymG}g^p=e_G$, which contains at least $e_G$.
 
 Now, \cref{lem:fixedptsize} claims that $p$ divides the cardinality of $X^{\CG_p}$, and since there \emph{are} fixed points, there must be
 at least $p$ fixed points.  One of them is the trivial one (given by $g\defeq e_G$ above), but the others are nontrivial.
@@ -172,7 +172,7 @@ \section{Cauchy's theorem}
 
 \footnote{Two slight variations commented away.  Have to choose one.  The first needs some background essentially boiling down to $BC_n$ being the truncation of the $n$th Moore space.
 % ALTERNATIVELY:
-%   Consider  the $p-1$-fold product $(\bn{(p-1)}\to \USym G)$ of $\USym G$ with itself.  We give this set the structure of a $\ZZ/p$-set as follows: ((here it is convenient to say that a $\ZZ/p$-set is the same as a $\ZZ$-set commuting with the $p$-fold cover)) define $X:S^1\to\Set$ by $X(\base)\defequi (\bn{(p-1)}\to \USym G)$ and by setting $X(\Sloop)$ to be the element in $X(\base)=(\base)$ sending $(g_1,\dots,g_{p-1})$ to $(g_2,\dots,g_{p-1},(g_1\cdots g_{p-1})^{-1})$.  Note that
+%   Consider  the $p-1$-fold product $(\bn{(p-1)}\to \USymG)$ of $\USymG$ with itself.  We give this set the structure of a $\ZZ/p$-set as follows: ((here it is convenient to say that a $\ZZ/p$-set is the same as a $\ZZ$-set commuting with the $p$-fold cover)) define $X:S^1\to\Set$ by $X(\base)\defequi (\bn{(p-1)}\to \USymG)$ and by setting $X(\Sloop)$ to be the element in $X(\base)=(\base)$ sending $(g_1,\dots,g_{p-1})$ to $(g_2,\dots,g_{p-1},(g_1\cdots g_{p-1})^{-1})$.  Note that
 % $$\xymatrix{S^1\ar[d]_{(-)^p}\ar[dr]^X&\\S^1\ar[r]_X&\Set}$$
 % commutes and so we get a $\ZZ/p$-action ((expand)).  A fixed point of this action is an element of $X(\base)$ of the form $(g,g,\dots,g)$ such that $g^{p-1}=g^{-1}$  (expand)). The choice $g=e$ always gives such a fixed point, but if there is any other point ... (do you need decidability here?), the pointed map $S^1\to \BG$ given by sending $\Sloop$ to $g$ gives the desired subgroup. Hence we need to show that $X$ has fixed points.
 
@@ -184,16 +184,16 @@ \section{Cauchy's theorem}
 % ALTERNATIVELY:
 % Recall the cyclic group of order $p$.  For the sake of convenience, we identify $\bn p\times\bn 1$ and $\bn p$, so that elements will be denoted $0,1,2,\dots$ and not $(0,0), (1,0),(2,0)\dots$, and we also write $s$ instead of $\sqrt[p]{\id}$ for the element in $\bn p=\bn p$ that shifts to the successor (mod $p$).  In other words we choose an identification $\zet/p=(\bn p,s)$ once and for all.  If
 % $$(S,j):BC_p\defequi\sum_{S:\UU}\sum_{j:X=X}||(S,j)=(\bn p,s)||,$$ consider the set
-% $$X(S,j)\defequi\sum_{g:S\to \USym G}||\sum_{a:(S,j)=(\bn p,s)}g_{a^{-1}(0)}\cdot\dots\cdot g_{a^{-1}(p-1)}=e_G||.$$
-% Note that if $g:\bn p\to\USym G$, then we have an equality of propositions
+% $$X(S,j)\defequi\sum_{g:S\to \USymG}||\sum_{a:(S,j)=(\bn p,s)}g_{a^{-1}(0)}\cdot\dots\cdot g_{a^{-1}(p-1)}=e_G||.$$
+% Note that if $g:\bn p\to\USymG$, then we have an equality of propositions
 % $$||\sum_{a:(\bn p,s)=(\bn p,s)}g_{a^{-1}(0)}\cdot\dots\cdot g_{a^{-1}(p-1)}=e_G||=g_{0}\cdot\dots\cdot g_{p-1}=e_G$$
 % since $(g_1\cdot\dots\cdot g_{p-1}=e_G)=(g_2\cdot\dots\cdot g_{p-1}\cdot g_1=e_G)$,
 % and so
-% $$X(\bn p,s)=\sum_{g:\bn p\to \USym G}g_{0}\cdot\dots\cdot g_{p-1}=e_G$$
-% which is equivalent to the $p-1$-fold product of $\USym G$ with itself ($g_0=(g_1\cdot\dots\cdot g_{p-1})^{-1}$, but all the other $g_i$s are then chosen arbitrarily).  Consequently, the number of elements in $X(\bn p,s)$ is divisible by $p$.
+% $$X(\bn p,s)=\sum_{g:\bn p\to \USymG}g_{0}\cdot\dots\cdot g_{p-1}=e_G$$
+% which is equivalent to the $p-1$-fold product of $\USymG$ with itself ($g_0=(g_1\cdot\dots\cdot g_{p-1})^{-1}$, but all the other $g_i$s are then chosen arbitrarily).  Consequently, the number of elements in $X(\bn p,s)$ is divisible by $p$.
 
 % Now, a $C_p$-fixed point of $X(\bn p,s)$ is an element $(g_0,\dots,g_{p-1},!)$ such that $(g_0,\dots,g_{p-1},!)=(g_1,\dots,g_{p-1},g_0,!)$, \ie $g_0=g_1=g_2=\dots=g_{p-1}$\footnote{if I am allowed to write that}.  In other words, a fixed point is of the form $(g,\dots,g,!)$, where $!$ expresses that $g^p=e_G$:
-% $$X(\bn p,s)^{C_p}=\sum_{g:\USym G}g^p=e_G.$$  If we can show that $(g,!):X(\bn p,s)^{C_p}$ is nonempty, we'd have established an abstract cyclic subgroup consisting of the powers of $g$.  Of course, setting $g=e_G$ will give us such a fixed point.
+% $$X(\bn p,s)^{C_p}=\sum_{g:\USymG}g^p=e_G.$$  If we can show that $(g,!):X(\bn p,s)^{C_p}$ is nonempty, we'd have established an abstract cyclic subgroup consisting of the powers of $g$.  Of course, setting $g=e_G$ will give us such a fixed point.
 
 %  Now, $X(\bn p,s)$ splits as a disjoint union of its orbits.  Since $p$ is prime, the group $C_p$ is simple ((where proved?)), and so the orbits are either singletons (fixed points) or free orbits:
 % $$X(\bn p,s)= X(\bn p,s)^{C_p}+(\text{free part of }X(\bn p,s)).$$
@@ -209,7 +209,7 @@ \section{Cauchy's theorem}
 \begin{proof}
   Recall the $G$-set $\Ad_G:\BG\to\Set$ given by $\Ad_G(z)=(z=z)$.
 Then the map
-$$\ev_{\shape_G}:\prod_{z:\BG}(z=z)\to\USym G,\quad \ev_G(f)=f(\shape_G)$$
+$$\ev_{\shape_G}:\prod_{z:\BG}(z=z)\to\USymG,\quad \ev_G(f)=f(\shape_G)$$
 has the structure of a (n abstract) inclusion of a subgroup; namely the inclusion of the center $Z(G)$ in $G$.
 The center thus represents the fixed points of the $G$-set $\Ad_G$.
 Since $G$ has \gporder a power of $p$, all orbits but the fixed points have cardinality divisible by $p$.
@@ -221,7 +221,7 @@ \section{Cauchy's theorem}
 \end{corollary}
 \begin{proof}
   The center $Z(G)$ is by \cref{lem:nontrivcenter} of \gporder $p$ or $p^2$.
-  Since $G$ is not cyclic we have that $g^p=e_G$ for all $g:\USym G$.
+  Since $G$ is not cyclic we have that $g^p=e_G$ for all $g:\USymG$.
 \footnote{((To be continued: the classical proof involves choosing nontrivial elements  -- see what can be done about that.  At present this corollary is not used anywhere))}
 \end{proof}
 \section{Sylow's Theorems}
diff --git a/group.tex b/group.tex
index 04f5440..46a2898 100644
--- a/group.tex
+++ b/group.tex
@@ -1962,7 +1962,7 @@ \section{Infinity groups (\texorpdfstring{\inftygps}{∞-groups})}
 \label{sec:inftygps}
 
 Disregarding the requirement that the classifying type
-of a group $G$ is a groupoid (so that $\USym G$ is a set)
+of a group $G$ is a groupoid (so that $\USymG$ is a set)
 we get the simpler notion of \inftygps:
 \begin{definition}\label{def:inftygps}
   The type of $\infty$-groups is
@@ -2050,7 +2050,7 @@ \section{$G$-sets}
 Note that in this case $\cdot: (x=y)\to X(x) \to X(y)$.
 See \cref{def:principaltorsor} for a special case
 where $\cdot_X$ is indeed path composition.}
-In particular, if $g:\USym G$,
+In particular, if $g:\USymG$,
 then $X(g)$ is a permutation of the underlying set of $X$.
 
 The type of $G$-sets is
@@ -2148,13 +2148,13 @@ \section{$G$-sets}
 is a $G$-set, and the value at $\shape_G$ is identified with $X$.
 \marginnote{%
 We must be careful not to focus too much on the underlying set.
-For instance, even though the underlying set of both $\Ad_G$ and $\princ G$ is $\USym G$, in general  $\Ad_G$ and $\princ G$  are very different $G$-sets.
-To drive this point home, compare the illustrations of transport along a $p:\USym G$ for the two:
+For instance, even though the underlying set of both $\Ad_G$ and $\princ G$ is $\USymG$, in general  $\Ad_G$ and $\princ G$  are very different $G$-sets.
+To drive this point home, compare the illustrations of transport along a $p:\USymG$ for the two:
 $$\xymatrix{\shape_G\ar@{=}[r]^p_\to\ar@{=}[d]_q^\downarrow&\shape_G\ar@{=}[d]^{\Ad_G(p)(q)}_\downarrow\\
   \shape_G\ar@{=}[r]^p_\to&\shape_G} $$%\qquad
 $$\xymatrix{\shape_G\ar@{=}[r]^{\refl{\shape_G}}_\to\ar@{=}[d]_q^\downarrow&\shape_G\ar@{=}[d]^{\princ G(p)(q)}_\downarrow\\
 \shape_G\ar@{=}[r]^p_\to&{\hphantom{.}}\shape_G.}$$
-A third $G$-set with underlying set $\USym G$ is $\mathrm{triv}_G(\USym G)$.}
+A third $G$-set with underlying set $\USymG$ is $\mathrm{triv}_G(\USymG)$.}
 
 The constructions in the previous two paragraphs yields the following equivalence:
 \[
@@ -2168,7 +2168,7 @@ \section{$G$-sets}
 \end{xca}
 
 \begin{xca}
-  Prove that a group $G$ is abelian group if and only if the $G$-sets $\Ad_G$ and $\mathrm{triv}_G(\USym G)$ are identical.
+  Prove that a group $G$ is abelian group if and only if the $G$-sets $\Ad_G$ and $\mathrm{triv}_G(\USymG)$ are identical.
 \end{xca}
 
 \sususe{Transitive $G$-sets}
@@ -2189,15 +2189,15 @@ \section{$G$-sets}
 connectedness (cf.~\cref{xca:component-connected}) it is enough to
 demand
 \begin{displaymath}
-  \exists_{b:X(\shape_G)}\prod_{a:X(\shape_G)}\exists_{g:\USym G}a=g\cdot b.
+  \exists_{b:X(\shape_G)}\prod_{a:X(\shape_G)}\exists_{g:\USymG}a=g\cdot b.
 \end{displaymath}
 In other words, $X$ is transitive if and only if there exists a
-$b:X(\shape_G)$ such that the map $-\cdot b:\USym G\to X(\shape_G)$ is
+$b:X(\shape_G)$ such that the map $-\cdot b:\USymG\to X(\shape_G)$ is
 surjective.
 
 Yet another equivalent way of expressing that $X$ is transitive
 is to say that $X(\shape_G)$ is nonempty and for any $a,b:X(\shape_G)$
-there exists some $g:\UG$ with $a = g\cdot b$.
+there exists some $g:\USymG$ with $a = g\cdot b$.
 \end{remark}
 
 \begin{lemma}
@@ -2212,7 +2212,7 @@ \section{$G$-sets}
   all $z:\BG$ and $a:X(z)$ there exists a $g:y=z$ such that $a=g\cdot b$.
   Since $\BG$ is connected, this is equivalent to asserting that there
   exists a $b:X(\shape_G)$ such that for all $a:X(\shape_G)$ there exists
-  a $g:\USym G$ such that $a=g\cdot b$.
+  a $g:\USymG$ such that $a=g\cdot b$.
 \end{proof}
 
 Recall that for type families $X,X':T\to\UU$, and
@@ -2260,7 +2260,7 @@ \subsection{Actions in a type}
 \end{definition}
 
 \begin{example}
-  An action of $G$ on its set $\USym G$ of symmetries is provided by taking $X$ to be the principal torsor $\princ G$ as defined in
+  An action of $G$ on its set $\USymG$ of symmetries is provided by taking $X$ to be the principal torsor $\princ G$ as defined in
   \cref{def:principaltorsor}.
 \end{example}
 
@@ -2447,11 +2447,11 @@ \subsection{Homomorphisms and torsors}
   \label{rem:inducedGsetfromabstracthomomorphisms}
   Notice that our construction of the induced $G$-set works equally well for a homomorphism $\phi:\Hom^\abstr(\abstr(G),\abstr(H))$:
   if $X:\BG\to\Set$ is a $G$-set, then we define the $H$-set $\phi_*X:\BH\to\Set$ by
-  $$\phi_*X(y)\defequi(\shape_H=y)\times_{\USym G}X(\shape_G)$$
+  $$\phi_*X(y)\defequi(\shape_H=y)\times_{\USymG}X(\shape_G)$$
   to be the set quotient of $(\shape_H=y)\times X(\shape_G)$ by the relation $(p,x)\sim(p\, \phi(q)^{-1},X(q)x)$ for all $q:\shape_G=pt_G$.
   Just as above, for $X$ the principal $G$-torsor we get an identity  $\eta_\phi:\phi_*\princ G=\princ H$ which, when evaluated at $y:\BH$, corresponds under univalence to the equivalence
-$$(\shape_H=y)\times_{\USym G}\USym G\to (\shape_H=y)$$
-sending $[p,q]:(\shape_H=y)\times_{\USym G}\USym G$ to $p\,\phi(q):(\shape_H=y)$.
+$$(\shape_H=y)\times_{\USymG}\USymG\to (\shape_H=y)$$
+sending $[p,q]:(\shape_H=y)\times_{\USymG}\USymG$ to $p\,\phi(q):(\shape_H=y)$.
 \end{remark}
 
 
@@ -2488,8 +2488,8 @@ \section{Groups; concrete vs.~abstract% -- same gem, different wrapping
   If $G$ is a group we can unravel the definition and see that an $\abstr(G)$-set consists of
   \begin{enumerate}
   \item a set $S$,
-  \item a function $f:\USym G\to (S=S)$
-  \item such that $f(e_G)=\refl{S}$ and for all $p,q:\USym G$ we have that $f(p\, q)=f(p)\,f(q)$.
+  \item a function $f:\USymG\to (S=S)$
+  \item such that $f(e_G)=\refl{S}$ and for all $p,q:\USymG$ we have that $f(p\, q)=f(p)\,f(q)$.
   \end{enumerate}
 
 \end{example}
@@ -2507,7 +2507,7 @@ \section{Groups; concrete vs.~abstract% -- same gem, different wrapping
 
 \begin{example}\label{ex:qG}
   If $G$ is a group, then for any $x:\BG$ the principal $G$-torsor \emph{evaluated at $x$}, \ie the set $\princ Gx\defequi(\shape_G=x)$, has a natural structure of an $\abstr(G)$-set by means of
-  $$\preinv:\USym G\to ((\shape_G=x)=(\shape_G=x))$$ and the fact that $\preinv(e_G)\defequi\refl{\shape_G=x}$ and that for $p,q:\USym G$ we have that
+  $$\preinv:\USymG\to ((\shape_G=x)=(\shape_G=x))$$ and the fact that $\preinv(e_G)\defequi\refl{\shape_G=x}$ and that for $p,q:\USymG$ we have that
   \marginnote{\ie if $r\colon \shape_G=x$ we have that
 $\preinv(p\, q)(r)=r(p\,q)^{-1}=r\,q^{-1}p^{-1}=\preinv(p)\preinv(q)(r)$  -- demonstrating why we chose $\preinv$: without the inverse this would have gone badly wrong.}
   $$\preinv(p\,q)=\preinv(p)\preinv(q).$$
@@ -2517,7 +2517,7 @@ \section{Groups; concrete vs.~abstract% -- same gem, different wrapping
 
 Though it sounded like we made a choice ending up with $\preinv$; we really didn't -- it is precisely what happens when you abstract the homomorphism $G\to\Sigma_{\princ G(x)}$:
 you get the function of identity types
-$$\USym G\to (\princ G(x)=\princ G(x))$$
+$$\USymG\to (\princ G(x)=\princ G(x))$$
 which by the very definition of transport for $\princ G$ is $\preinv$.
 \end{example}
 
@@ -2590,7 +2590,7 @@ \section{Homomorphisms; abstract vs.~concrete}
 They do, and we provide two independent and somewhat different arguments.  Translating from group homomorphisms to abstract group homomorphisms is easy: if $G$ and $H$ are groups, then we defined
 $$\abstr:\Hom(G,H)\to\Hom^\abstr(\abstr(G),\abstr(H))$$
 in \cref{def:abstrisfunctor} as the function which takes a homomorphism, aka a pointed map $f=(\Bf_\div,p_f):\BG\ptdto\BH$ to the induced map of identity types
-$$\US f\defequi \mathrm{ad}_{p_f}\ap{\Bf_\div}:\USym G\to\USym H$$
+$$\US f\defequi \mathrm{ad}_{p_f}\ap{\Bf_\div}:\USymG\to\USymH$$
  together with the proofs that this is an abstract group homomorphism from $\abstr(G)$ to $\abstr(H)$, c.f~\cref{def:abstrisfunctor}.
 
 
@@ -2753,8 +2753,8 @@ \section{Homomorphisms; abstract vs.~concrete}
 Consider the map
 $$A:((\typetorsor_G,\princ G))\to_*(\typetorsor_H,\princ H)\to \Hom^\abstr(\abstr(G),\abstr(H))$$
 given by letting $A(f,p)$ be the composite
-$$\xymatrix{\USym G\ar@{=}[d]^{\pathsp{}^G}_\downarrow&&&
-  \USym H\ar@{=}[d]^{\pathsp{}^H}_\downarrow\\
+$$\xymatrix{\USymG\ar@{=}[d]^{\pathsp{}^G}_\downarrow&&&
+  \USymH\ar@{=}[d]^{\pathsp{}^H}_\downarrow\\
   (\princ G=\princ G)\ar[r]^-f&
   (f\princ G=f\princ G)\ar@{=}[rr]^-{q\mapsto p^{-1}qp}_\to&&
   (\princ H=\princ H)
@@ -2769,13 +2769,13 @@ \section{Homomorphisms; abstract vs.~concrete}
 be given by $B(\phi,!)=(\phi_*X,\eta_\phi)$
 
 We show that $A$ and $B$ are inverse equivalences.  Given an abstract group homomorphism $(\phi,!):\Hom^\abstr(\abstr(G),\abstr(H))$, then $AB(\phi,!)$ has as underlying set map
-$$\xymatrix{\USym G\ar@{=}[d]^{\pathsp{}^G}_\downarrow&&&
-  \USym H\ar@{=}[d]^{\pathsp{}^H}_\downarrow\\
+$$\xymatrix{\USymG\ar@{=}[d]^{\pathsp{}^G}_\downarrow&&&
+  \USymH\ar@{=}[d]^{\pathsp{}^H}_\downarrow\\
   (\princ G=\princ G)\ar[r]^-{\phi_*}&
   (\phi_*\princ G=\phi_*\princ G)\ar@{=}[rr]^-{q\mapsto \eta_\phi^{-1}q\eta_\phi}_\to&&
   (\princ H=\princ H),
 }$$
-and if we start with a $g:\USym G$, then $\pathsp{}^G$ sends it to $\pathsp g^G\oldequiv\preinv (g)$.  Furthermore, $\phi_*\preinv (g)$ is $[\id,\preinv (g)]$ which is sent to $\preinv (\phi(g))$ in $\princ H=\princ H$ which corresponds to $\phi(g):\USym H$ under $\pathsp{}^H$.  In other words, $AB(\phi,!)=(\phi,!)$.  The composite $BA$ is similar.
+and if we start with a $g:\USymG$, then $\pathsp{}^G$ sends it to $\pathsp g^G\oldequiv\preinv (g)$.  Furthermore, $\phi_*\preinv (g)$ is $[\id,\preinv (g)]$ which is sent to $\preinv (\phi(g))$ in $\princ H=\princ H$ which corresponds to $\phi(g):\USymH$ under $\pathsp{}^H$.  In other words, $AB(\phi,!)=(\phi,!)$.  The composite $BA$ is similar.
 \end{proof}
 
 
@@ -2824,12 +2824,12 @@ \section{Monomorphisms and epimorphisms}
 \]
 \end{definition}
 
-\marginnote{$$\xymatrix{\USym G\ar[d]^\simeq\ar[r]^{\US f}&\USym H\ar[d]^\simeq\\
+\marginnote{$$\xymatrix{\USymG\ar[d]^\simeq\ar[r]^{\US f}&\USymH\ar[d]^\simeq\\
     \Hom(\ZZ,G)\ar[r]^{f_*}\ar[d]^\simeq_\abstr&\Hom(\ZZ,H)\ar[d]^\simeq_\abstr\\
     \Hom^{\abstr}(\ZZ,\abstr(G))\ar[r]^{\abstr f_*}&\Hom^{\abstr}(\ZZ,\abstr(H))
  }$$
 commutes (we've written $\ZZ$ also for $\abstr(\ZZ$) since otherwise it wouldn't fit.}
-We've seen that for any group $G$, the underlying set $\USym G\defequi(\shape_G=\shape_G)$ of $\abstr(G)$ is equivalent to the set of homomorphisms $\Hom(\ZZ,G)$ which in turn is equivalent to the set of abstract homomorphisms $\Hom^{\abstr}(\abstr(\ZZ),\abstr(G))$ and that abstraction preserves composition.
+We've seen that for any group $G$, the underlying set $\USymG\defequi(\shape_G=\shape_G)$ of $\abstr(G)$ is equivalent to the set of homomorphisms $\Hom(\ZZ,G)$ which in turn is equivalent to the set of abstract homomorphisms $\Hom^{\abstr}(\abstr(\ZZ),\abstr(G))$ and that abstraction preserves composition.
 Hence, if $f:\Hom(G,H)$ is a group homomorphism, then saying that
 $\US f$ is an injection is equivalent to saying that postcomposition by $f$ is an injection $\Hom(\ZZ,G)\to\Hom(\ZZ,H)$.
 In this observation, the integers $\ZZ$ plays no more of a r\^ole than $\bn 1$ does in \cref{lem:injofsetsaremono}; we can let the source vary over any group $F$:
@@ -2840,7 +2840,7 @@ \section{Monomorphisms and epimorphisms}
 The following propositions are equivalent:\label{lem:eq-epi-conn}
 \begin{enumerate}
 \item\label{it:mono} $f$ is a monomorphism;
-\item\label{it:injection} $\US f:\USym G\to\USym H$ is an injection;
+\item\label{it:injection} $\US f:\USymG\to\USymH$ is an injection;
 \item\label{it:cover} $\Bf_\div:\BG_\div\to \BH_\div$ is a \covering.
 \end{enumerate}
 \end{lemma}
@@ -2864,7 +2864,7 @@ \section{Monomorphisms and epimorphisms}
   The following propositions are equivalent:
 \begin{enumerate}[label=(\arabic*')]
 \item\label{it:epi} $f$ is an epimorphism;
-\item\label{it:surjection} $\US f:\USym G\to\USym H$ is a surjection.
+\item\label{it:surjection} $\US f:\USymG\to\USymH$ is a surjection.
 \item\label{it:connfib} $\Bf_\div:\BG_\div\to \BH_\div$ has connected fibers.
 \end{enumerate}
 \end{lemma}
@@ -2915,9 +2915,9 @@ \section{Monomorphisms and epimorphisms}
     \varphi_\pt \defeq \refl{\sh_G,\cst{\sh_A}}, \quad
     \psi_\pt \defeq (\refl{\sh_G}, j\pi).
   \]
-  The equalizer of $\varphi$ and $\psi$ thus consists of all $g:\UG$
-  such that $j\pi(gg') = j\pi(g')$ for all $g':\UG$. Since $j$ is injective,
-  this is equivalent to $\pi(gg')=\pi(g')$ for all $g':\UG$, and this holds
+  The equalizer of $\varphi$ and $\psi$ thus consists of all $g:\USymG$
+  such that $j\pi(gg') = j\pi(g')$ for all $g':\USymG$. Since $j$ is injective,
+  this is equivalent to $\pi(gg')=\pi(g')$ for all $g':\USymG$, and this holds
   if and only if $g$ belongs to $H$.
 \end{proof}
 
@@ -2929,25 +2929,25 @@ \subsection{Any symmetry is a symmetry in $\Set$}
 % \footnote{which reminds me of the following: my lecturer in cosmology once tried to publish a paper about rotating black holes, only to have it rejected because it turned out that it was his universe, not the black hole, that was rotating}
 
 Recall the principal $G$-torsor $\princ G:\BG\to\Set$.
-Since $\princ G(\shape_G)\defequi \USym G$ this defines a pointed function $\rho_G:\BG\to_* \BSigma_{\USym G}\defequi(\conncomp \Set {\USym G},\USym G)$,
+Since $\princ G(\shape_G)\defequi \USymG$ this defines a pointed function $\rho_G:\BG\to_* \BSigma_{\USymG}\defequi(\conncomp \Set {\USymG},\USymG)$,
 \marginnote{the letter $\rho$ commemorates the word ``regular''} \ie a homomorphism from $G$ to the permutation group
-$$\rho_G:\Hom(G,\Sigma_{\USym G}).$$
+$$\rho_G:\Hom(G,\Sigma_{\USymG}).$$
 \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 $\USym G$ in $\Set$ is an injection, \ie ``any symmetry is a symmetry in $\Set$''.}Let $G$ be a group. Then
-  $\rho_G:\Hom(G,\Sigma_{\USym G})  $ is a monomorphism.
+  \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,\Sigma_{\USymG})  $ is a monomorphism.
 \end{theorem}
 \begin{proof}
-  In view of \cref{lem:eq-mono-cover} we need to show that $\rho_G:\BG\to \conncomp \Set {\USym G}$ is a
+  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)\oldequiv (\conncomp{\Set}{\USym G},\USym G)$$ of
+  $$\bar{\pathsp{}}:\BG=(\typetorsor_G,\princ G)\oldequiv (\conncomp{\Set}{\USymG},\USymG)$$ of
   \cref{lem:BGbytorsor}, $\rho_G$ translates to the
   evaluation map
-  $$\mathrm{ev}_{\shape_G}:\conncomp{(\BG\to\Set)}{\princ G}\to\conncomp{\Set}{\USym G},\qquad
+  $$\mathrm{ev}_{\shape_G}:\conncomp{(\BG\to\Set)}{\princ G}\to\conncomp{\Set}{\USymG},\qquad
   \mathrm{ev}_{\shape_G}(E)=E(\shape_G).$$
   We must show that the preimages
-  $\inv{\ev_{\shape_G}}(X)$ for $X:\Sigma_{\USym G}$ are sets.  This
+  $\inv{\ev_{\shape_G}}(X)$ for $X:\Sigma_{\USymG}$ are sets.  This
   fiber is equivalent to
   $\sum_{E:\conncomp{(\BG\to\Set)}{\princ G}}(X=E(\shape_G))$ which is a
   set precisely when $\sum_{E:\BG\to\Set}(X=E(\shape_G))$ is a set.  We
@@ -3034,7 +3034,7 @@ \subsection{Center of a group}
 every $p:\refl{\BG_\div}\eqto\refl{\BG_\div}$, the following proposition
 holds:
 \begin{displaymath}
-  \prod_{g:\USym G }p(\shape_G) g = g p(\shape_G)
+  \prod_{g:\USymG }p(\shape_G) g = g p(\shape_G)
 \end{displaymath}
 In other words, $\abstr{(\grpcenterinc G)}$ maps elements of
 $\abstr(Z(G))$ to elements of $\abstr(G)$ that commute with every
@@ -3091,8 +3091,8 @@ \subsection{Center of a group}
 center'' of $G$ is picked out by $\abstr{(\grpcenterinc G)}$.
 \begin{lemma}
   \label{lemma:center-inc-surj-on-paths}%
-  Let $g:\USym G$ and suppose that $gh=hg$ for every
-  $h:\USym G$. The fiber $\inv{(\ap {\B\grpcenterinc G})}(g)$ contains
+  Let $g:\USymG$ and suppose that $gh=hg$ for every
+  $h:\USymG$. The fiber $\inv{(\ap {\B\grpcenterinc G})}(g)$ contains
   an element.
 \end{lemma}
 \begin{proof}
@@ -3108,8 +3108,8 @@ \subsection{Center of a group}
     family $T$,
   \item aim to prove $\iscontr(\sum_{u:x\eqto x}T(u))$ for any $x:\BG$,
   \item this is a proposition, so connectedness of $\BG$ can be applied
-    and only $\iscontr(\sum_{u:\USym G}T(u))$ needs to be proven,
-  \item hopefully, $\sum_{u:\USym G}T(u)$ reduces to an obvious
+    and only $\iscontr(\sum_{u:\USymG}T(u))$ needs to be proven,
+  \item hopefully, $\sum_{u:\USymG}T(u)$ reduces to an obvious
     singleton type.
   \end{enumerate}
   Here, for any $x:\BG$, we define the type family $T: (x\eqto x) \to \UU$
@@ -3123,23 +3123,23 @@ \subsection{Center of a group}
   the following composition of equivalences:
   \begin{displaymath}%
     \begin{aligned}
-      \sum_{q:\USym G}T(q) &\jdeq
-      \sum_{q:\USym G}\prod_{p:\USym G}(pg=qp)
+      \sum_{q:\USymG}T(q) &\jdeq
+      \sum_{q:\USymG}\prod_{p:\USymG}(pg=qp)
       \\
-      &\equivto \sum_{q:\USym G}\prod_{p:\USym G}(g=q)
+      &\equivto \sum_{q:\USymG}\prod_{p:\USymG}(g=q)
       \\
-      &\equivto \sum_{q:\USym G}\USym G\to (g=q)
+      &\equivto \sum_{q:\USymG}\USymG\to (g=q)
       \\
-      &\equivto \sum_{q:\USym G}\Trunc{\USym G}\to (g=q)
+      &\equivto \sum_{q:\USymG}\Trunc{\USymG}\to (g=q)
       \\
-      &\equivto \sum_{q:\USym G} (g=q)
+      &\equivto \sum_{q:\USymG} (g=q)
       \\
       &\equivto 1
     \end{aligned}
   \end{displaymath}%
   % \marginnote[-10\baselineskip]{%
   In that composition, the first equivalence is using that $g$ commutes with
-  every other element $p:\USym G$, so that $pg \inv p = g$. The second
+  every other element $p:\USymG$, so that $pg \inv p = g$. The second
   equivalence acknowledges the fact that the codomain $(g=q)$ does not depend on
   $p$ anymore, so that the dependent function type inside the sum is a simple
   function type. The third equivalence uses the universal property of
@@ -3152,7 +3152,7 @@ \subsection{Center of a group}
   contractible. We define now $\hat g(x):x\eqto x$ as the chosen center of
   contraction of that type. More precisely, by connectedness of $\BG$, the
   inverse $\inv\varphi$ of the exhibited equivalence
-  $\varphi:\sum_{q:\USym G}T(q) \equivto 1$ produces a dependent function of
+  $\varphi:\sum_{q:\USymG}T(q) \equivto 1$ produces a dependent function of
   type $\prod_{x:\BG}1\equivto \sum_{q: x\eqto x}T(q)$, and $\hat g$ is the
   pointwise evaluation at the unique element $\triv$ of $1$. In particular,
   $\hat g (\shape_G) = \inv\varphi (\triv) = g$ as wanted.
@@ -3163,7 +3163,7 @@ \subsection{Center of a group}
 $\abstr{(\grpcenterinc G)}$ establishes an equivalence
 \begin{equation}
   %\left( \id_{\BG_\div} = \id_{\BG_\div} \right)
-  \USym \grpcenter(G) \equivto \sum_{g:\USym G}\prod_{h:\USym G}gh=hg
+  \USym \grpcenter(G) \equivto \sum_{g:\USymG}\prod_{h:\USymG}gh=hg
 \end{equation}
 In yet other words,
 $\B \grpcenter(G)\defequi \conncomp{(\BG_\div \eqto \BG_\div)}
@@ -3183,7 +3183,7 @@ \subsection{Center of a group}
 % a group $G$ is abelian if and only if it satisfies the following
 % property:
 % \begin{displaymath}
-%   \prod_{g,h:\USym G}gh=hg
+%   \prod_{g,h:\USymG}gh=hg
 % \end{displaymath}
 % which is the ordinary definition of an abstract abelian group in
 % ordinary group theory.
@@ -3756,9 +3756,9 @@ \section{$G$-sets vs $\abstr(G)$-sets}
   Let $G$ be a group.  Then the map
   $$\ev_{\shape_G}:\GSet\to\Set^\abstr_{\abstr(G)},\qquad \ev_{\shape_G}(X)\defequi(X(\shape_G),a_X)
 $$
-is an equivalence, where the homomorphism $a_X:\Hom^\abstr(\abstr(G), \abstr(\Sigma_{X(\shape_G)}))$ is given by transport $X:\USym G\defequi(\shape_G=\shape_G)\to (X(\shape_G)=X(\shape_G))$.
+is an equivalence, where the homomorphism $a_X:\Hom^\abstr(\abstr(G), \abstr(\Sigma_{X(\shape_G)}))$ is given by transport $X:\USymG\defequi(\shape_G=\shape_G)\to (X(\shape_G)=X(\shape_G))$.
 \end{lemma}
-If $X$ is a $G$-set, $g:\USym G$ and $x:X(\shape_G)$, we seek forgiveness for writing $g\cdot x:X(\shape_G)$ instead of $\cast(a_X(g))(x)$.\footnote{and I ask forgiveness for strongly disliking the use of ``$\cast$'' as a name for some tacitly understood map!}
+If $X$ is a $G$-set, $g:\USymG$ and $x:X(\shape_G)$, we seek forgiveness for writing $g\cdot x:X(\shape_G)$ instead of $\cast(a_X(g))(x)$.\footnote{and I ask forgiveness for strongly disliking the use of ``$\cast$'' as a name for some tacitly understood map!}
 
 \begin{example}
   \label{ex:abstrandconj}
@@ -3768,15 +3768,15 @@ \section{$G$-sets vs $\abstr(G)$-sets}
 What abstract $\abstr(G)$-set does this correspond to?
 In particular, under the equivalence $\abstr:\Hom(H,G)\to\Hom^\abstr(\abstr(H),\abstr(G))$, what is the corresponding action of $\abstr(G)$ on the abstract homomorphisms?
 
-The answer is that $g:\USym G$ acts on $\Hom^\abstr(\abstr(H),\abstr(G))$ by postcomposing with conjugation $\conj^g$ by $g$ as defined in \cref{ex:conjhomo}.
+The answer is that $g:\USymG$ acts on $\Hom^\abstr(\abstr(H),\abstr(G))$ by postcomposing with conjugation $\conj^g$ by $g$ as defined in \cref{ex:conjhomo}.
 
 Let us spell this out in some detail:
 If $(F,p):\Hom(H,G)(\shape_G)\defequi
- \sum_{F:\BH_\div\to \BG_\div}(\shape_G=F(\shape_H))$ and $g:\USym G$, then $g\cdot(F,p)\defequi(F,p\,g^{-1})$.  If we show that the action of $g$ sends $\abstr(F,p)$ to $\conj^g\circ\abstr(F,p)$ we are done.
+ \sum_{F:\BH_\div\to \BG_\div}(\shape_G=F(\shape_H))$ and $g:\USymG$, then $g\cdot(F,p)\defequi(F,p\,g^{-1})$.  If we show that the action of $g$ sends $\abstr(F,p)$ to $\conj^g\circ\abstr(F,p)$ we are done.
 
 Recall that $\abstr(F,p)$ consists of the composite
-$$\xymatrix{\USym H\ar[r]^-{F^=}&(F(\shape_H)=F(\shape_G))\ar[rr]^-{t\mapsto p^{-1}t\,p}&&\USym G},$$
-(\ie $\abstr(F,p)$ applied to $q:\USym H $ is  $p^{-1}F^=(q)\,p$)  together with the proof that this is an abstract group homomorphism.
+$$\xymatrix{\USymH\ar[r]^-{F^=}&(F(\shape_H)=F(\shape_G))\ar[rr]^-{t\mapsto p^{-1}t\,p}&&\USymG},$$
+(\ie $\abstr(F,p)$ applied to $q:\USymH $ is  $p^{-1}F^=(q)\,p$)  together with the proof that this is an abstract group homomorphism.
 We see that $\abstr(F,p\,g^{-1})$ is given by conjugation:
 $q\mapsto(p\,g^{-1})^{-1}F^=(q)\,(p\,g^{-1})=g\,(p^{-1}F^=(q)\,p)\,g^{-1}$, or in other words $\conj^g\circ\abstr(F,p)$.
 \end{example}
@@ -3786,7 +3786,7 @@ \section{$G$-sets vs $\abstr(G)$-sets}
 \end{lemma}
 
 If $f:\Hom(G,G')$ is a homomorphism, then precomposition with $\Bf:\BG\to \BG'$ defines a map $$f^*:(G'\text{-}\Set)\to(G\text{-}\Set).$$
-\marginnote{Recall that \cref{lem:eq-mono-cover} told us that $f$ is an epimorphism precisely when $\USym f$ is a surjection.}
+\marginnote{Recall that \cref{lem:eq-mono-cover} told us that $f$ is an epimorphism precisely when $\USymf$ is a surjection.}
 We will have the occasion to use the following result which essentially says that if $f:\Hom(G,G')$ is an epimorphism, then $f^*$ embeds the type of $G'$-sets as some of the components of the type of $G$-sets.
 \begin{lemma}
   \label{lem:epifullyfaithful}
@@ -3803,12 +3803,12 @@ \section{$G$-sets vs $\abstr(G)$-sets}
  is the likewise injective, so $f^*:(X=Y)\to(f^*X=f^*Y)$ is injective.
 
 For surjectivity, let $F':f^*X=f^*Y$ and write, for typographical convenience, $a:X(f(\shape_G)=Y(f(\shape_G))$ for $\mathrm{ev}_{\shape_G}F'\defequi F'_{\shape_G}$.
-By the equivalence between $G$-sets and $\abstr(G)$-sets, $F'$ is uniquely pinned down by $a$ and the requirement that for all $g'=f(g)$ with $g:\USym G$ the diagram
+By the equivalence between $G$-sets and $\abstr(G)$-sets, $F'$ is uniquely pinned down by $a$ and the requirement that for all $g'=f(g)$ with $g:\USymG$ the diagram
 $$\xymatrix{X(f(\shape_G))\ar@{=}[r]^{X({g'})}\ar@{=}[d]_{a}&
   X(f(\shape_G))\ar@{=}[d]_{a}\\
   Y(f(\shape_G))\ar@{=}[r]^{Y({g'})}&Y(f(\shape_G))}
 $$
-commutes.  Likewise, (using transport along the identity $p_f:\shape_{G'}=f(\shape_G)$) an $F:X=Y$ in the preimage of $a$ is pinned down by the commutativity of the same diagram, but with $g':f(\shape_G)=f(\shape_G)$ arbitrary (an a priori more severe requirement, again reflecting injectivity).   However, when $f:\USym G\to\USym {G'}$ is surjective these requirements coincide, showing that $f^*$ is an equivalence.
+commutes.  Likewise, (using transport along the identity $p_f:\shape_{G'}=f(\shape_G)$) an $F:X=Y$ in the preimage of $a$ is pinned down by the commutativity of the same diagram, but with $g':f(\shape_G)=f(\shape_G)$ arbitrary (an a priori more severe requirement, again reflecting injectivity).   However, when $f:\USymG\to\USymG'$ is surjective these requirements coincide, showing that $f^*$ is an equivalence.
 
 
 % Fix for the moment an  $a:X(f(\shape_G)=Y(f(\shape_G))$
@@ -3817,7 +3817,7 @@ \section{$G$-sets vs $\abstr(G)$-sets}
 %   X(f(\shape_G))\ar@{=}[d]_{F'_{f(\shape_G)}}\\
 %   Y(f(\shape_G))\ar@{=}[r]^{Y_{g'}}&Y(f(\shape_G))}
 % $$
-% commutes.  Likewise, an identity $F:f^*X=f^*Y$ is given by exactly the same data, except that the diagram is only required to commute for $g'=f(g)$ for all $g:\USym G$.  But when $f:\USym G\to\USym {G'}$ these requirements coincide.
+% commutes.  Likewise, an identity $F:f^*X=f^*Y$ is given by exactly the same data, except that the diagram is only required to commute for $g'=f(g)$ for all $g:\USymG$.  But when $f:\USymG\to\USymG'$ these requirements coincide.
 
 
 % ; $F:X=Y$ is in the preimage of $a:X(f(\shape_G)=Y(f(\shape_G))$ if and only if $a=F_{f(\shape_G)}$ and for all $g':f(\shape_G)=f(\shape_G)$ the diagram
@@ -3825,11 +3825,11 @@ \section{$G$-sets vs $\abstr(G)$-sets}
 %   X(f(\shape_G))\ar@{=}[d]_{F_{f(\shape_G)}}\\
 %   Y(f(\shape_G))\ar@{=}[r]^{Y_{g'}}&Y(f(\shape_G))}
 % $$
-% commutes.  However, since $f$ is surjective there is a $g:\USym G$ so that $g'=f(g)$.  Therefore, anything in $f^*X=f^*Y$ which is in the preimage of $a$ is in the image of $f^*:X=Y$ and we have shown that $f^*$ is also a surjection.
+% commutes.  However, since $f$ is surjective there is a $g:\USymG$ so that $g'=f(g)$.  Therefore, anything in $f^*X=f^*Y$ which is in the preimage of $a$ is in the image of $f^*:X=Y$ and we have shown that $f^*$ is also a surjection.
 \end{proof}
 
 \section{Semidirect products}
-\label{sec:Semidirect-products}{\color{red} just moved without proofreading BID 211116}
+\label{sec:Semidirect-products}{\color{red} just moved without proofreading BID 211116. Problem with $\USym$ followed by composite MAB 240815.}
 
 In this section we describe a generalization of the product of two group, called the {\em semidirect} product, which can be constructed from an
 action of a group on a group.  Like the product, it consists of pairs, both at the level of concrete groups and of abstract groups, as we shall
@@ -3945,12 +3945,12 @@ \section{Semidirect products}
 \end{proof}
 
 Our next goal is to present the explicit formula for the multiplication operation in $\USym { G \ltimes \tilde H }$.
-First we apply \cref{lem:pathpairsection} to get a bijection $\USym { G \ltimes \tilde H } \weq \USym G \times \USym H$.
-Now use that to transport the multiplication operation of the group $\USym { G \ltimes \tilde H }$ to the set $\USym G \times \USym H$.
+First we apply \cref{lem:pathpairsection} to get a bijection $\USym { G \ltimes \tilde H } \weq \USymG \times \USymH$.
+Now use that to transport the multiplication operation of the group $\USym { G \ltimes \tilde H }$ to the set $\USymG \times \USymH$.
 Now \cref{lem:pathpairsectionmult} tells us the formula for that transported operation is given as follows.
 $$ (p',q') \cdot (p,q) = (p' \cdot p , ({q'} ^ p) \cdot q) $$
 In a traditional algebra course dealing with abstract groups, this formula is used as the definition of the multiplication operation
-on the set $\USym G \times \USym H$, but then one must prove that the operation satisfies the properties of \cref{def:abstractgroup}.
+on the set $\USymG \times \USymH$, but then one must prove that the operation satisfies the properties of \cref{def:abstractgroup}.
 The advantage of our approach is that the formula emerges from the underlying logic that governs how composition of paths works.
 
 
@@ -4133,7 +4133,7 @@ \section{Sums of groups}
 \begin{corollary}
   \label{cor:ZplusZuniv}
   If $G$ is a group, then the functions
-  $$\Hom(\ZZ\vee\ZZ,G)\to \Hom(\ZZ,G)\times\Hom(\ZZ,G)\simeq \USym G\times \USym G$$
+  $$\Hom(\ZZ\vee\ZZ,G)\to \Hom(\ZZ,G)\times\Hom(\ZZ,G)\simeq \USymG\times \USymG$$
   is an equivalence.
 \end{corollary}
 
@@ -4177,16 +4177,16 @@ \section{Sums of groups}
 
 Let $C_1$ be the set of strings $(p_0,n,p_1,\dots,p_n)$ with $n:\NN$ and, for $0\leq j\leq n$
 \begin{itemize}
-\item $p_{j}:\USym G_1%\defequi (a_1=a_1)
+\item $p_{j}:\USymG_1%\defequi (a_1=a_1)
   $  for even $j$
-\item $p_{j}:\USym G_2%\defequi (a_2=a_2)
+\item $p_{j}:\USymG_2%\defequi (a_2=a_2)
   $ for odd $j$ and
 \item $p_j$ is not reflexivity for $j$ positive
 \end{itemize}
 (the last requirement makes sense and is a proposition since our groups are decidable).
 
-  Then the function given by composition in $\USym G_{12}\defequi(a_{12}=a_{12})$
-  $$\beta:C_1\to\USym G_{12}%\defequi(a_{12}=a_{12})
+  Then the function given by composition in $\USymG_{12}\defequi(a_{12}=a_{12})$
+  $$\beta:C_1\to\USymG_{12}%\defequi(a_{12}=a_{12})
   ,\qquad\beta(p_0,n,p_1,\dots p_n)\defequi i_1^gp_0i_2^gp_1i_1^gp_2\dots i_?^gp_n$$
 (where $i_?^gp_n$  is $i_1^gp_n$ or $i_2^gp_n$ according to whether $n$ is even or odd) is an equivalence.
 \end{lemma}
@@ -4329,7 +4329,7 @@ \section{Heaps \texorpdfstring{$(\dagger)$}{(\textdagger) \color{red} just moved
 In fact, this map lifts to the type of heaps with a chosen identification.
 \begin{exercise}\label{xca:group+torsor-heap}
   Define natural equivalences $\Heap \weq \sum_{G:\Group}\BG$,
-  and $\Group \weq \sum_{H:\Heap}(\USym H)$.
+  and $\Group \weq \sum_{H:\Heap}(\USymH)$.
 \end{exercise}
 Recalling the equivalence between $\BG$ and the type of $G$-torsors
 from~\cref{lem:BGbytorsor},
@@ -4346,8 +4346,8 @@ \section{Heaps \texorpdfstring{$(\dagger)$}{(\textdagger) \color{red} just moved
 
 Here's an \emph{a priori} different map from heaps to groups:
 For a heap $H$, consider all the
-symmetries of the underlying set of identifications $\USym H$
-that arise as $r \mapsto p\inv q r$ for $p,q\in \USym H$.
+symmetries of the underlying set of identifications $\USymH$
+that arise as $r \mapsto p\inv q r$ for $p,q\in \USymH$.
 
 Note that $(p,q)$ and $(p',q')$ determine the same symmetry
 if and only if $p\inv q = p'\inv{q'}$, and if and only if
@@ -4381,11 +4381,11 @@ \section{Heaps \texorpdfstring{$(\dagger)$}{(\textdagger) \color{red} just moved
 
 \begin{exercise}\label{xca:heap-variety}
   Fix a set $S$.
-  Show that the fiber $\inv{\USym}(S)\jdeq\sum_{H:\Heap}(S=\USym H)$ is a set.
+  Show that the fiber $\inv{\USym}(S)\jdeq\sum_{H:\Heap}(S=\USymH)$ is a set.
 
   Now fix in addition a ternary operation $t:S\times S\times S\to S$ on $S$.
   Show that the fiber of the map $\Heap \to \sum_{S:\Set}(S\times S\times S \to S)$,
-  mapping $H$ to $(\USym H,(p,q,r)\mapsto p \inv{q} r)$,
+  mapping $H$ to $(\USymH,(p,q,r)\mapsto p \inv{q} r)$,
   at $(S,t)$ is a proposition,
   and describe this proposition in terms of equations.
 \end{exercise}
diff --git a/subgroups.tex b/subgroups.tex
index 0ecdb57..73c7ca1 100644
--- a/subgroups.tex
+++ b/subgroups.tex
@@ -41,7 +41,7 @@ \subsection{Subgroups as monomorphisms}
   $$\typeepi_G\defequi\sum_{H:\typegroup}\sum_{f:\Hom(G,G')}\isepi(f).$$
   A monomorphism $(H,i,!)$ is
       \begin{enumerate}
-      \item \emph{trivial}\index{trivial monomorphism} if $H$ is the trivial group, %.contractible (or, equivalently, if $\USym H$ is contractible),
+      \item \emph{trivial}\index{trivial monomorphism} if $H$ is the trivial group, %.contractible (or, equivalently, if $\USymH$ is contractible),
       \item \emph{proper}\index{proper monomorphism} if $i$ is not an isomorphism.\qedhere
       \end{enumerate}
     \end{definition}
@@ -94,7 +94,7 @@ \subsection{Subgroups as monomorphisms}
 }\isEq(\US f)\times (i_{H'}\eqto{}i_H f)$ a proposition.
 % Consequently, the identity type
 % $(H,i_H,!)\eqto{}_{\typesubgroup_G}(H,i_H,!)$ is equivalent to the type of homomorphisms $f:\Hom(H,H)$ which are such that $!:i_H^==i_H^=f^=$ and such that $f^=$ is an equivalence (as we see in a moment this last requirement is redundant).
-% Now, since $(H,i_H,!)$ is a subgroup, $i_H^=$ is an injection of sets, which forces $!:f^==\refl{\USym H}$, which ultimately forces $f$ to be (identical to) the identity homomorphism.
+% Now, since $(H,i_H,!)$ is a subgroup, $i_H^=$ is an injection of sets, which forces $!:f^==\refl{\USymH}$, which ultimately forces $f$ to be (identical to) the identity homomorphism.
 \end{proof}
 
 \subsection{Subgroups through $G$-sets}
@@ -134,7 +134,7 @@ \subsection{Subgroups through $G$-sets}
     given by $A\mapsto\sum_{B:\FinSet 2}(A\eqto{}B+\bn 1)$ together with a proof that this is a set; in fact, the identity type $(B,p)\eqto{}(B',p')$ is equivalent to $\sum_{q:B\eqto{}B'}(q+\bn 1)p\eqto{}p'$ which is a proposition since $q$ is uniquely given by $q+\bn 1\eqto{}p'p^{-1}$.
   \end{example}
   \begin{xca}
-    Given a group $G$ we defined in \cref{sec:groupssubperm} a monomorphism from $G$ to the permutation group $\Aut_{\USym G}(\Set)$. Write out the corresponding subgroup of $\Aut_{\USym G}(\Set)$.
+    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}
 \begin{example}
   \label{ex:prodinclisGset}
@@ -371,7 +371,7 @@ \subsection{Kernels and cokernels}
 \end{corollary}
 \begin{xca}
   Let $f:\Hom(G,G')$.  Then the subgroup $E(\ker f):\typesubgroup_G$ associated with the kernel is given by a $G$-set equivalent to the one sending $x:\BG$ to
-  $$\sum_{p:\shape_{G'}\eqto{}\Bf(x)}\Trunc{\sum_{\beta:\shape_G\eqto{}x}p\eqto{}\USym f(\beta)p_f}.$$
+  $$\sum_{p:\shape_{G'}\eqto{}\Bf(x)}\Trunc{\sum_{\beta:\shape_G\eqto{}x}p\eqto{}\USymf(\beta)p_f}.$$
   If $f$ is an epimorphism this is furthermore equivalent to
   $$x\mapsto(\shape_{G'}\eqto{}\Bf(x)).$$
 \end{xca}
@@ -504,14 +504,14 @@ \subsection{The image}
   \item the following are equivalent
     \begin{enumerate}
     \item $f$ is an epimorphism,
-    \item $\USym f$ is a surjection
+    \item $\USymf$ is a surjection
     \item the cokernel of $f$ is contractible,
     \item the inclusion of the image $\incl_{\img f}:\Hom(\image f,G')$ is an isomorphism,
     \end{enumerate}
   \item the following are equivalent
     \begin{enumerate}
     \item $f$ is a monomorphism,
-    \item $\USym f$ is an injection
+    \item $\USymf$ is an injection
 \item the kernel of $f$ is trivial
 \item $\Bf:\BG\to \BG'$ is a \covering.
 \item the projection onto the image $\prj_{\img f}:\Hom(G,\Img f)$ is an isomorphism.
@@ -702,12 +702,12 @@ \section{The action on the set of subgroups}
   If $G$ is a group, then the action of $G$ on the set of monomorphisms into $G$ is called \emph{conjugation}\index{conjugation}.
 
   \label{def:conjugate}
-  If $(H,F,p,!):\typemono_G(\shape_G)$ is a monomorphism into $G$ and $g:\USym G$, then the monomorphisms  $(H,F,p,!),(H,F,p\,g^{-1},!):\typemono_G(\shape_G)$ are said to be \emph{conjugate}\index{conjugate}\index{conjugate}.
+  If $(H,F,p,!):\typemono_G(\shape_G)$ is a monomorphism into $G$ and $g:\USymG$, then the monomorphisms  $(H,F,p,!),(H,F,p\,g^{-1},!):\typemono_G(\shape_G)$ are said to be \emph{conjugate}\index{conjugate}\index{conjugate}.
 \end{definition}
 \begin{remark}
   \label{rem:whyconjugate}
   The term ``conjugation'' may seem confusing as the %(abstract)
-action of $g:\USym G$ on a monomorphism $(H,F,p,!):\typemono_G(\shape_G)$ (where $p:x\eqto{}F(\shape_H)$) is simply $(H,F,p\,g^{-1},!)$, which does not seem much like conjugation.
+action of $g:\USymG$ on a monomorphism $(H,F,p,!):\typemono_G(\shape_G)$ (where $p:x\eqto{}F(\shape_H)$) is simply $(H,F,p\,g^{-1},!)$, which does not seem much like conjugation.
 However, as we saw in \cref{ex:abstrandconj}, under the equivalence $\abstr:\Hom(H,G)\we\Hom^\abstr(\abstr(H),\abstr(G))$, the corresponding action on $\Hom^\abstr(\abstr(H),\abstr(G))$ is exactly (postcomposition with) conjugation $c^g:\abstr(G)\eqto{}\abstr(G)$.
 \footnote{The same phenomenon appeared in \cref{xca:HomZGvsAdG} where we gave an equivalence between the $G$-sets $\Hom(\ZZ,G)$ and $\Ad_G$ (where the action is very visibly by conjugation).}
   \label{rem:conjactiononmonos}
@@ -720,7 +720,7 @@ \section{The action on the set of subgroups}
 \end{lemma}
 \begin{remark}
   \label{rem:typeofsubgpstrivifab}
-  We know that a group $G$ is abelian if and only if conjugation is trivial: for all $g:\USym G$ we have $c^g\eqto{}\id$, and so we get that $\typemono_G$ is a trivial $G$-set if and only if $G$ is abelian.
+  We know that a group $G$ is abelian if and only if conjugation is trivial: for all $g:\USymG$ we have $c^g\eqto{}\id$, and so we get that $\typemono_G$ is a trivial $G$-set if and only if $G$ is abelian.
 \end{remark}
 
 The subgroup analog of $y\mapsto\typemono_G(y)$ is
@@ -1271,7 +1271,7 @@ \section{Intersecting with normal subgroups}
 
 \begin{lemma}
   \label{lem:thereisaconjugate}
-  Let $G$ be a group, $X:\BG\to Set$ a $G$-set, $x:X(\shape_G)$, $g:\USym G$ and $H\eqto{}(H,F,p,!):\typesubgroup_G$ a subgroup of $G$ ($F:\BH_\div\to \BG_\div$ and $p:\shape_G\eqto{}F(\shape_H)$).
+  Let $G$ be a group, $X:\BG\to Set$ a $G$-set, $x:X(\shape_G)$, $g:\USymG$ and $H\eqto{}(H,F,p,!):\typesubgroup_G$ a subgroup of $G$ ($F:\BH_\div\to \BG_\div$ and $p:\shape_G\eqto{}F(\shape_H)$).
 
 Then $g\,x$ is a fixed point for the $H$-action on $X$ if and only if $x$ is a fixed point for the action  of the conjugate subgroup $g\,H\defequi(H,F,g^{-1}p_F,!)$ on $X$.
 \end{lemma}
diff --git a/symmetry.tex b/symmetry.tex
index 603f006..a1f2371 100644
--- a/symmetry.tex
+++ b/symmetry.tex
@@ -70,7 +70,7 @@
 % \end{definition}
 
 % \begin{example}
-%   An action of $G$ on its set $\USym G$ of symmetries is provided by taking $X$ to be the principal torsor $\princ G$ as defined in
+%   An action of $G$ on its set $\USymG$ of symmetries is provided by taking $X$ to be the principal torsor $\princ G$ as defined in
 %   \cref{def:principaltorsor}.
 % \end{example}
 
@@ -179,7 +179,7 @@
 % In fact, this map lifts to the type of heaps with a chosen identification.
 % \begin{exercise}\label{xca:group+torsor-heap}
 %   Define natural equivalences $\Heap \weq \sum_{G:\Group}\BG$,
-%   and $\Group \weq \sum_{H:\Heap}(\USym H)$.
+%   and $\Group \weq \sum_{H:\Heap}(\USymH)$.
 % \end{exercise}
 % Recalling the equivalence between $\BG$ and the type of $G$-torsors
 % from~\cref{lem:BGbytorsor},
@@ -196,8 +196,8 @@
 
 % Here's an \emph{a priori} different map from heaps to groups:
 % For a heap $H$, consider all the
-% symmetries of the underlying set of identifications $\USym H$
-% that arise as $r \mapsto p\inv q r$ for $p,q\in \USym H$.
+% symmetries of the underlying set of identifications $\USymH$
+% that arise as $r \mapsto p\inv q r$ for $p,q\in \USymH$.
 
 % Note that $(p,q)$ and $(p',q')$ determine the same symmetry
 % if and only if $p\inv q = p'\inv{q'}$, and if and only if
@@ -231,11 +231,11 @@
 
 % \begin{exercise}\label{xca:heap-variety}
 %   Fix a set $S$.
-%   Show that the fiber $\inv{\USym}(S)\jdeq\sum_{H:\Heap}(S=\USym H)$ is a set.
+%   Show that the fiber $\inv{\USym}(S)\jdeq\sum_{H:\Heap}(S=\USymH)$ is a set.
 
 %   Now fix in addition a ternary operation $t:S\times S\times S\to S$ on $S$.
 %   Show that the fiber of the map $\Heap \to \sum_{S:\Set}(S\times S\times S \to S)$,
-%   mapping $H$ to $(\USym H,(p,q,r)\mapsto p \inv{q} r)$,
+%   mapping $H$ to $(\USymH,(p,q,r)\mapsto p \inv{q} r)$,
 %   at $(S,t)$ is a proposition,
 %   and describe this proposition in terms of equations.
 % \end{exercise}
@@ -355,12 +355,12 @@
 % \end{proof}
 
 % Our next goal is to present the explicit formula for the multiplication operation in $\USym { G \ltimes \tilde H }$.
-% First we apply \cref{lem:pathpairsection} to get a bijection $\USym { G \ltimes \tilde H } \weq \USym G \times \USym H$.
-% Now use that to transport the multiplication operation of the group $\USym { G \ltimes \tilde H }$ to the set $\USym G \times \USym H$.
+% First we apply \cref{lem:pathpairsection} to get a bijection $\USym { G \ltimes \tilde H } \weq \USymG \times \USymH$.
+% Now use that to transport the multiplication operation of the group $\USym { G \ltimes \tilde H }$ to the set $\USymG \times \USymH$.
 % Now \cref{lem:pathpairsectionmult} tells us the formula for that transported operation is given as follows.
 % $$ (p',q') \cdot (p,q) = (p' \cdot p , ({q'} ^ p) \cdot q) $$
 % In a traditional algebra course dealing with abstract groups, this formula is used as the definition of the multiplication operation
-% on the set $\USym G \times \USym H$, but then one must prove that the operation satisfies the properties of \cref{def:abstractgroup}.
+% on the set $\USymG \times \USymH$, but then one must prove that the operation satisfies the properties of \cref{def:abstractgroup}.
 % The advantage of our approach is that the formula emerges from the underlying logic that governs how composition of paths works.
 
 \section{The orbit-stabilizer theorem}