done 3.10

circle.tex

@@ -3522,40 +3522,46 @@ \section{Universal property of $\Cyc_n$}
   %
   \marginnote{The construction of $f$ is really a special case
   of the delooping of the abstract group homomorphism 
-  $\sigma_n^i \mapsto \sigma^i$ in \cref{}.}
+  $\sigma_n^i \mapsto \sigma^i$ in \cref{sec:delooping}.}
 
   Finally, we prove that the fiber $\inv{\ev_{n,A}}(a,\sigma,!)$ is a
-  proposition. As we just proved that it is inhabited, we would have
-  successfully shown that the fiber is contractible. Given two elements
-  $(f,p,!)$ and $(f',p',!)$ of the fiber, we want to find a path between the
-  two, that is $\chi:\prod_{x:\Cyc_n} f(x) \eqto f'(x)$ such that the following
-  commutes:
-  \begin{displaymath}
+  proposition. Let $(f,p,!)$ and $(f',p',!)$
+  be two elements of the fiber. We want to identify them.
+  From the proofs in their third
+  components we infer $p\sigma\inv p = \ap{f}(\sigma_n)$ and
+  $p'\sigma\inv {p'} = \ap{f'}(\sigma_n)$, respectively.
+  Define the family of sets $U(x)\defequi (f(x) \eqto f'(x))$
+  parametrized by $x:\Cyc_n$.
+  It suffices to find a $\chi:\prod_{x:\Cyc_n} U(x)$
+  such that the diagram in the margin commutes.
+  \begin{marginfigure}
     \begin{tikzcd}
       a \rar[eqr,"p"] \dar[eql,"p'"'] & f(\pt_n) \dlar[eqr,"\chi(\pt_n)"]\\
       f'(\pt_n) &
     \end{tikzcd}
-  \end{displaymath}
-  Let us denote $U(x)\defequi f(x) \eqto f'(x)$ for $x:\Cyc_n$, and notice that
-  these types are sets (as $A$ is a groupoid). The element $\tau\defequi p'\inv
-  p : U(\pt_n)$ is peculiar in that  $\trp[U] q (\tau) = \tau$ for all $q:\pt_n\eqto\pt_n$.
-  Indeed, we use once
-  again that symmetries of $\pt_n$ in $\Cyc_n$ are of the form $\sigma_n^i$ and
-  we calculate:
+  \end{marginfigure}
+  The element $\tau\defequi p'\inv p : U(\pt_n)$ is peculiar in that 
+  $\trp[U] q (\tau) = \tau$ for all $q:\pt_n\eqto\pt_n$.
+  Indeed, we use once again that symmetries of $\pt_n$ in $\Cyc_n$ are 
+  of the form $\sigma_n^i$ and we calculate:
   \begin{displaymath}
-    \trp[U] {\sigma_n^i} (\tau) = \ap {f'} (\sigma_n^i) \cdot \tau \cdot \inv{\ap {f}(\sigma_n^i)}
-    = p' \sigma^i \inv {p'} \cdot p'\inv p p \sigma^{-i} \inv p = p' \inv p
+    \trp[U] {\sigma_n^i} (\tau) = 
+    \ap {f'} (\sigma_n^i) \cdot \tau \cdot \inv{\ap {f}(\sigma_n^i)}
+    = p' \sigma^i \inv {p'} \tau p \sigma^{-i} \inv p = p' \inv p
   \end{displaymath}
   Now it is easy to prove that the following type is contractible:
   \begin{displaymath}
-    V(x) \defequi \sum_{\alpha: U(x)} \alpha = \trp[U] \blank (\tau).
+    V(x) \defequi \sum_{\alpha: U(x)} \prod_{r:\pt_n\eqto x}
+    \alpha = \trp[U] r (\tau)
   \end{displaymath}
   To do so, we use the connectedness of $\Cyc_n$ and verify the contractibility
-  of $V(\pt_n)$ by pointing out that $V(\pt_n)$ is simply the singleton type of
-  $\tau$. Now $\chi$ is defined as the function mapping $x$ to the center of
-  contraction of $V(x)$. By definition, $\chi(\pt_n) = \tau$ as we wanted.
+  of $V(\pt_n)$. Clearly, $(\tau,!)$ is a center of contraction 
+  by the peculiarity of $\tau$. Also, if $\alpha$ and $\beta$ are
+  elements of $V(\pt_n)$, then $\alpha=\beta$ by taking $r\jdeq\refl{pt_n}$. 
+  Now $\chi$ is defined as the function mapping $x$ to 
+  the center of contraction of $V(x)$, so that $\chi(\pt_n) = \tau$ as we wanted.
   %
-  \marginnote{The construction of $\chi$ is really an ad hoc version of the following fact: for any $G$-set $X$, the type of fixed points of $X$ is equivalent to the type of sections of $\sum_{z:\BG}X(z) \to \BG$. If we move this section forward, one can rewrite it as such.}
+  \marginnote{The construction of $\chi$ is really an ad hoc version of the following fact: for any $G$-set $X$, the type of fixed points of $X$ is equivalent to the type of sections of $\sum_{z:\BG}X(z) \to \BG$. If we move this section forward, one can rewrite it as such. TO DO}
 \end{proof}
 
 As a direct corollary, we can classify the connected \coverings over $\Cyc_n$ for finite orders $n$.