trival group Aut_Prop(True)

group.tex

@@ -428,11 +428,11 @@ \subsection{First examples}
   \begin{enumerate}
   \item\label{ex:trivgroup}
   Recall that $\true$, and hence $\true \eqto \true$, is contractible.
-  Hence $\Aut_{\Set}(\true)$ is a group called the 
+  Hence $\Aut_\Prop(\true)$ is a group called the 
   \emph{trivial group}. \index{trivial group}
   In fact, for any proposition $P$ we can also identify the trivial group 
-  with $\Aut_{\Set}(P)$, see \cref{xca:group-example-details}. 
-  Unlike $\Set$, the type $\true$ is connected,
+  with $\Aut_\Prop(P)$, see \cref{xca:group-example-details}. 
+  Unlike $\Prop$, the type $\true$ is connected,
   so we can also identify the trivial group with
   $\mkgroup (\true,\triv)$, or with $\mkgroup (C,c)$ for
   any contractible type $C$ and element $c:C$, or
@@ -442,10 +442,10 @@ \subsection{First examples}
 Recall from \cref{sec:universes} the chain of
 universes $\UU_0 : \UU_1 : \UU_2 : \dots$ such that for each $i$
 all types in $\UU_i$ are also in $\UU_j$ for all $j>i$.
-Let $\Set_0$ be the type of sets in $\UU_0$, 
-\ie $\Set_0\defeq \sum_{S:\UU_0}\isset(S)$. Then $\true:\Set_0$ 
-and $\Set_0 : \UU_1$ (because the sum is taken over $\UU_0$).
-In order to accommodate the trivial group $\Aut_{\Set_0}(\true)$, 
+Let $\Prop_0 \defeq \sum_{P:\UU_0}\isprop(P)$ be the type of 
+propositions in $\UU_0$. Then $\true:\Prop_0$ 
+and $\Prop_0 : \UU_1$ (because the sum is taken over $\UU_0$).
+In order to accommodate the trivial group $\Aut_{\Prop_0}(\true)$, 
 the universe ``$\UU$'' appearing as a subscript of the first 
 $\Sigma$-type in \cref{def:pt-conn-groupoid}, reappearing later in 
 \cref{def:typegroup} of the type of groups,
@@ -515,7 +515,7 @@ \subsection{First examples}
 
 \begin{xca}
   \label{xca:group-example-details}
-  Show that $\Aut_{\Set}(P)$ is a trivial group for any proposition $P$.
+  Show that $\Aut_\Prop(P)$ is a trivial group for any proposition $P$.
   Verify that $\SG_0$, $\SG_1$, and $\SG_\false$ are all trivial groups.
   Using~\cref{def:finiteset}, give identifications of type 
   $\Aut_\FinSet(\bn{n})\eqto\Sigma_{\bn{n}}$ for $n:\NN$.