Fix diagram and proof of Theorem 3.3.8 (set bundle over circle)

circle.tex

@@ -706,17 +706,17 @@ \section{\Coverings}
   \bigl(\Sc\to\UU \ar[r,equivr,"g"]\bigr) & 
   \sum_{X:\UU}(X\equivto X) \ar[u,hookrightarrow]                         
 \\
-  \SetBundle \ar[r,equivl,"f"'] \ar[u,hookrightarrow]  &
+  \SetBundle(\Sc) \ar[r,equivl,"f"'] \ar[u,hookrightarrow]  &
   \bigl(\Sc\to\Set\bigr) \ar[r,equivl,"g"'] \ar[u,hookrightarrow]  &
   \sum_{X:\Set}(X\equivto X) \ar[u,hookrightarrow]
 \end{tikzcd}
 \]
 \end{theorem}
 \begin{proof}
 We prove first that $\preim$ respects the subtypes. 
-Let $A:\UU$ and $h: \Sc\to A$ such that $(A,h)$ is a \covering.
-This means that $\inv h(a)$ is a set, for any $a:A$.
-Since $\preim(A,h)(a) \jdeq \inv h(a)$, we immediately get
+Let $A:\UU$ and $h: A \to \Sc$ such that $(A,h)$ is a \covering.
+This means that $\inv h(x)$ is a set, for any $x:\Sc$.
+Since $\preim(A,h)(x) \jdeq \inv h(x)$, we immediately get
 that $\preim(A,h) : \Sc\to\Set$. 
 In order to prove that $\inv\preim$ also respects the subtypes
 one simply reverses this argument.