start with 5.7

actions.tex

@@ -1621,15 +1621,15 @@ \section{The orbit-stabilizer theorem}
 
 Let $G$ be a group (or $\infty$-group) and  $X : \BG \to \UU$  a $G$-type.
 Recall the orbit type of \cref{def:orbittype} $X_{hG}\defequi
-\sum_{z:\BG}X(z)$ and its truncation, the set of orbits $X / G \defeq \Trunc{X_{hG}}_0$ and the map $X(\shape_G)\to X_{hG}$ sending $x:X(\shape_G)$ to $[x]\defequi (\shape_G,x)$.
+\sum_{z:\BG}X(z)$ and its truncation, the set of orbits $X / G \defeq \setTrunc{X_{hG}}$ and the map $X(\shape_G)\to X_{hG}$ sending $x:X(\shape_G)$ to $[x]\defequi (\shape_G,x)$.
 
 
 For an element $x:X/G$ consider the associated subtype of $X(\shape_G)$ consisting of
- all $y : X(\shape_G)$ so that $|[y]|$ is equal to $x$ in the set of orbits:
+ all $y : X(\shape_G)$ so that $\settrunc{[y]}$ is equal to $x$ in the set of orbits:
 \[
-  \mathcal O_{x} \defeq \sum_{y : X(\shape_G)} x =_{X/G} |[y]|.
+  \mathcal O_{x} \defeq \sum_{y : X(\shape_G)} x =_{X/G} \settrunc{[y]}.
 \]
- For a point $x : X(\shape_G)$, we call $G\cdot x \defeq \mathcal O_{|[x]|}$ 
+ For a point $x : X(\shape_G)$, we call $G\cdot x \defeq \mathcal O_{\settrunc{[x]}}$ 
  the \emph{orbit through $x$}\index{orbit through $x$}.
  % as the subtype of $X(\shape_G)$ consisting of
 %  all $y : X(\shape_G)$ so that $[y]$ is equal to $[x]$ in the set of orbits: