Fix some typos and add a reference in circle.tex

circle.tex

@@ -551,7 +551,7 @@ \section{\Coverings}
 two points (i.e., each preimage can be merely identified with $\bool$).
 However, $A$ is not the constant family, like $A'$ depicted on the right,
 since we have a string of equivalences
-$A'\defeq\sum_{z:\Sc}\bool\eqto(\Sc\times\bool)\eqto(\Sc+\Sc)$,
+$A'\defeq\sum_{z:\Sc}\bool\eqto(\Sc\times\bool)\eqto(\Sc\amalg\Sc)$,
 and the latter type is not connected.
 Obviously something way more fascinating is going on.
 
@@ -578,7 +578,7 @@ \section{\Coverings}
     \node[fill,circle,inner sep=1pt] at (-1,1) {};
 %    \node (L) at (1,-3) {(left)};
     \begin{scope}[xshift=6cm]
-    \node (At) at (2,1) {$\Sc+\Sc$};
+    \node (At) at (2,1) {$\Sc\amalg\Sc$};
     \node (Bt) at (2,-2) {$\Sc$};
     \draw[->] (At) -- (Bt);
     \draw (0,-2) ellipse (1 and .3);
@@ -1162,7 +1162,7 @@ \section{The symmetries in the circle}
 
 We note in passing that combining the above two exercises
 yields an equivalence from $(\Sc\eqto\Sc)$ to $(\Sc\amalg\Sc)$,
-that is, a characterization of the symmetries \emph{of} the cycle
+that is, a characterization of the symmetries \emph{of} the circle
 (in constrast to the title of this \cref{sec:symcirc}).
 
 
@@ -2144,7 +2144,7 @@ \section{Connected \coverings over the circle}
   The Limited Principle of Omniscience (\cref{LPO})
   implies that the type of connected decidable \coverings over the circle is the sum
 of the component containing the universal \covering and for each positive integer $m$,
-the component containing the $m$-fold \covering.
+the component containing the $m$-fold \covering (\cref{def:mfoldS1cover}).
 \end{lemma}
 
 \begin{remark}