fix footnote on ttac

intro-uf.tex

@@ -1431,7 +1431,10 @@ \section{Equivalences}\label{sec:equivalence}
   $x:X$ and $y:Y$.
   Construct an equivalence of type $\bigl(\prod_{x:X}\sum_{y:Y}Z(x,y)\bigr)
   \equivto \sum_{f:X\to Y}\prod_{x:X}Z(x,f(x))$.\footnote{%
-  This equivalence is called the set-theoretic axiom of choice.}
+    This equivalence is sometimes called the type-theoretic axiom of choice;
+    more prosaically, it expresses the distributivity of products ($\Pi$-types)
+    over sums ($\Sigma$-types).
+    We discuss the real axiom of choice in~\cref{sec:choicefin}.}
 \end{xca}
 
 \begin{xca}\label{xca:section-above-f}