From f28b980649741e4260b15ca8660d4ff1e4dbe6e3 Mon Sep 17 00:00:00 2001 From: Ulrik Buchholtz Date: Tue, 1 Oct 2024 12:42:08 +0100 Subject: [PATCH] tiny --- abelian.tex | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/abelian.tex b/abelian.tex index 696c688..372893f 100644 --- a/abelian.tex +++ b/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,