tiny = to eqto in circle

circle.tex

@@ -1565,7 +1565,8 @@ \section{A reinterpretation of the circle}\label{sec:S1isC}
 \begin{proof}
 Using \cref{cor:fib-vs-path}\ref{conn-fib-vs-path} it suffices to show that
 each map induced by $f$ on identity types is an equivalence if and only if the specific map
-$\ap f : (x=x) \to (f(x) = f(x))$ is an equivalence.  Being an equivalence is a proposition,
+$\ap f : (x\eqto x) \to (f(x) \eqto f(x))$ is an equivalence.
+Being an equivalence is a proposition,
 so the result follows in two easy steps from $X$ being connected,
 using \cref{xca:component-connected}.
 \end{proof}