Merge branch 'master' of github.com:UniMath/SymmetryBook

actions.tex

@@ -82,7 +82,7 @@ \section{Group actions ($G$-sets)}
   with \emph{underlying type} $X(\sh_G)$.
   More generally, an action of $G$ on an element of type $A$
   is a function $X : \BG\to A$, see~\cref{sec:actions} below.}
-  
+
 \begin{example}\label{def:trivGset}
   If $G$ is a group and $X$ is a set, then $\triv_G X$ defined by
   \[\triv_G X(z)\defequi X, \quad\text{for all $z:\BG$,}\]
@@ -217,7 +217,7 @@ \section{Group actions ($G$-sets)}
   then a
   \emph{map from $X$ to $Y$} is an element of the type
   \[
-  \prod_{z:\BG}(X(z)\to Y(z)).
+    \Hom_G(X,Y) \defeq \prod_{z:\BG}(X(z)\to Y(z)).
   \]
   When $f$ is such a map, we may write $f_z$ for $f(z)$.
   \index{map!of $G$-sets}\index{$G$-subset}
@@ -229,7 +229,7 @@ \section{Group actions ($G$-sets)}
   $x:X(z)$, $g:z\eqto w$. In other words, the following diagram commutes:
 \[
 \begin{tikzcd}
-  z\ar[d,eqr,"g"] &X(z) \ar[r,"f_z"] \ar[d,eql,"X(g)"'] 
+  z\ar[d,eqr,"g"] &X(z) \ar[r,"f_z"] \ar[d,eql,"X(g)"']
                   &Y(z) \ar[d,eqr,"Y(g)"] \\
   w               &X(w) \ar[r,"f_w"']                & Y(w)
 \end{tikzcd}
@@ -241,14 +241,14 @@ \section{Group actions ($G$-sets)}
 This applies to the following definition.
 \end{remark}
 
-\begin{definition}\label{def:Gsubset} 
-  A \emph{$G$-subset of $X$} is a map from $X$ to the $G$-set that is
-  constant $\Prop$. The type of all such maps is denoted by
+\begin{definition}\label{def:Gsubset}
+  A \emph{$G$-predicate of $X$} is a map from $X$ to the $G$-set that is
+  constant $\Prop$. The type of all such maps is denoted by%
+  \glossary(SubGX){$\protect\Sub_G(X)$}{set of $G$-subsets of $X$}
   \[
-   \Sub_{G,X}\defeq \prod_{z:\BG}(X(z)\to\Prop).
+   \Sub_G(X)\defeq \Hom_G(X,\triv_G\Prop) \jdeq \prod_{z:\BG}(X(z)\to\Prop).
   \]
-  %\glossary(Gsubsets){\protect{$\Sub_{G,X}$}}{set of $G$-subsets of $X$} ERROR
-  Similarly to \cref{cor:subtype-same-level}, $\Sub_{G,X}$ is a set.
+  Similarly to \cref{cor:subtype-same-level}, $\Sub_{G}(X)$ is a set.
   If $P$ is a $G$-subset of $X$, then the \emph{underlying $G$-set of $P$},
   denoted by $X_P$, is defined by
   \[
@@ -258,13 +258,12 @@ \section{Group actions ($G$-sets)}
 \end{definition}
 
 \begin{xca}\label{xca:SubGX-closedSubXshG}
-\MB{MB unsure this was what UB meant.}
-Show that evaluation at $\sh_G$ is an equivalence from $\Sub_{G,X}$ to 
+Show that evaluation at $\sh_G$ is an equivalence from $\Sub_G(X)$ to
 \[
-\sum_{Q:X(\sh_G)\to\Prop}
+  \sum_{Q:\Sub(X(\sh_G))}
   \prod_{x:X(\sh_G)}
-    \bigl(Q(x)\to\prod_{g:\USymG} Q(g\cdot x)\bigr).
-\] 
+  \Bigl(Q(x)\to\prod_{g:\USymG} Q(g\cdot x)\Bigr).
+\]
 The latter type is the type of all
 subsets of $X(\sh_G)$ that are closed under the group action.
 \end{xca}