tiny

abelian.tex

@@ -690,13 +690,13 @@ \subsection{Higher deloopings}
   equivalence $(TX, t) \ptdweto X$.
 \end{proof}
 
-\begin{exercise}\label{xca:sections-as-dependent-functions}
-  Recall that a {\em section} (see~\cref{def:surjection} and its
+\begin{xca}\label{xca:sections-as-dependent-functions}
+  Recall that a \emph{section} (see~\cref{def:surjection} and its
   accompanying footnote) of a function $f:A \to B$ is a function
   $s: B \to A$ together with an identification $f\circ s \eqto \id_B$.
   Construct an equivalence from the type $\secfun f$ of sections of
   $f$ to the type $\prod_{b:B}\sum_{a:A}b \eqto f(a)$.
-\end{exercise}
+\end{xca}
 
 Consider the evaluation function
 $\ev_{X_\div,Y} : (X_\div \eqto Y) \to Y$ (defined by path-induction,