minor

group.tex

@@ -2077,7 +2077,7 @@ \section{Infinity groups (\texorpdfstring{\inftygps}{∞-groups})}
   $\Bf : \BG\ptdto\BH$ the \emph{classifying map} of $f$.
 \end{definition}
 
-\section{$G$-sets}
+\section{Group actions ($G$-sets)}
 \label{sec:gsets}
 
 One of the goals of \cref{sec:Gsetforabstract} below
@@ -2284,12 +2284,12 @@ \subsection{Transitive $G$-sets}
 We hinted there that they are connected to subgroups, so
 we now study them over a general group $G$.
 As $G$-sets they are called transitive $G$-sets.
-Classically, a $\abstr(G)$-set (a notion \emph{we} have yet not defined) $\mathcal X$ is said to be \emph{transitive} if there exists a $b:\mathcal X$ such that for all $a:\mathcal X$ there exists a $g:\mathcal X$ with $a=g\cdot b$.  In our world this translates to:
+Classically, a $\abstr(G)$-set (a notion \emph{we} have yet not defined) $\mathcal X$ is said to be \emph{transitive} if there exists some $x:\mathcal X$ such that for all $y:\mathcal X$ there exists a $g:\mathcal X$ with $x=g\cdot y$.  In our world this translates to:
 \begin{definition}\label{def:transitiveGset}
   A $G$-set $X:\BG\to\Set$ is \emph{transitive}\index{transitive $G$-set} if the proposition
   \[
     \istrans(X) \defequi
-    \exists_{x:X(\shape_G)} \prod_{y:X(\shape_G)} \exists_{g:\USymG} a=g\cdot b
+    \exists_{x:X(\shape_G)} \prod_{y:X(\shape_G)} \exists_{g:\USymG} x=g\cdot y
   \]
   holds.
 \end{definition}

intro-uf.tex

@@ -2998,8 +2998,8 @@ \section{Decidability, excluded middle and propositional resizing}
   \label{pri:prop-resizing}\index{Propositional resizing}
   For any pair of nested universes $\UU:\UU'$, the map
   $(P\mapsto P):\Prop_\UU \to \Prop_{\UU'}$ is an equivalence.\footnote%
-  {The map $P\mapsto P$ is well-typed by \emph{cumulativity}
-  of the universes, that is, by point (\ref{it:cumulative})
+  {The map $P\mapsto P$ is welltyped by \emph{cumulativity}
+  of the universes, that is, by point~\ref{it:cumulative}
   of \cref{sec:universes}. Note that the map is not
   the identity function due to its type.}
 \end{principle}