small in 3.5

circle.tex

@@ -1483,17 +1483,16 @@ \section{A reinterpretation of the circle}\label{sec:S1isC}
 The equivalence $\preim$ maps $\cst\base$ to
 $(x:\Sc) \mapsto \sum_{\_:\bn 1}(x\eqto \base)$
 which can be identified with $\uc\base$.
-Now consider the following diagram
+Now consider the following diagram:
 \begin{equation}\label{eq:setbundle-Sc-univ-comp}
   \begin{tikzcd}
-    & \Sc\ar[dl,"\cst{\blank}"']\ar[d,"\uc{\blank}"]\ar[dr,"c"] & \\
-    \conncomp{\SetBundle(\Sc)}{\cst\base} \ar[r,"\sim"]
+    & \Sc\ar[dl,"{(\bn 1,\cst{\blank})}"']\ar[d,"\uc{\blank}"]\ar[dr,"c"] & \\
+    \conncomp{\SetBundle(\Sc)}{\bn1,\cst\base} \ar[r,"\sim"]
     & \conncomp{(\Sc\to\UU)}{\uc\base} \ar[r,"\sim","\ev_\UU"']
-    & \InfCyc,
+    & \InfCyc
   \end{tikzcd}
 \end{equation}
-where indeed the components in the last row are corresponding.
-
+%where the last row is indeed well defined.
 Both the left and the right triangle represent identity types.
 We have an identification for the left triangle
 because the fiber $\sum_{\_:\bn 1}(x\eqto z)$ of $\cst z$ at $x:\Sc$ can be identified with $\uc{z}(x) \jdeq (z\eqto x)$, for any $z:\Sc$.