polish

circle.tex

@@ -794,7 +794,7 @@ \section{\Coverings}
 
 \begin{lemma}\label{lem:univ-cover-of-groupoid}
 Let $(A,a_0)$ be a pointed type, $(B,b_0)$ a pointed
-groupoid, and $f : (A,a_0)\ptdto (B,b_0)$ a \covering. 
+groupoid, and $f : (A,a_0)\ptdto (B,b_0)$ a pointed \covering. 
 Then $f$ is universal if and only if $A$ is contractible. 
 \end{lemma}
 
@@ -811,7 +811,7 @@ \section{\Coverings}
 \cref{def:funext} to get an identification of type $f \eqto_{A\to B} gh$.
 The pointing path of $gh$ is also $g_0 : b_0 \eqto g(c_0)$.
 We get an identification of type $(f,f_0)\eqto_{A\ptdto B} (gh,g_0)$
-from an identification of $g_0 = (g_0\inv f_0) f_0$.%
+since $g_0 = (g_0\inv f_0) f_0$.%
 \marginnote{Draw the triangle!}
 The type $(A,a_0)\ptdto (C,c_0)$ is contractible since $A$ is
 contractible, yielding that $h$ is unique. 
@@ -907,92 +907,9 @@ \section{\Coverings}
 
 In the next section we will see that the exponential \covering
 of the circle is in fact universal.
-
-
-\subsection*{Old, discuss status 10.08.23}
-
-We already defined a \covering $f:A\to B$ to be universal if $A$ is connected
-and all $a\eqto_A a$ (for $a:A$) are connected.
-If moreover $B$ is a pointed, connected groupoid we shall argue that
-we actually can speak of \emph{the} universal \covering
-in \cref{def:universalcover}.
-
-Recall \cref{cor:fib-vs-path} stating that all the fibers of a map $f:A\to B$
-are sets if and only if each
-\[
-\ap{f}: (a=a')\to (f(a)=f(a'))
-\]
-is an injection.
-Assume $f:A\to B$ is a universal \covering and $B$ is a groupoid.
-We prove that $A$ is contractible.
-Being contractible is a proposition, so we may assume
-we have an element $a$ of $A$ since $A$ is connected.
-By \cref{xca:connected-trivia} and \ref{xca:component-connected}
-it suffices to prove that $a=a$ is contractible.
-By \cref{xca:connected-trivia-2}, using that $a=a$ is connected,
-it suffices to show that $a=a$ is a set.
-Using that $\ap{f}$ is an injection, we can apply the remark after
-\cref{lem:sum-of-fibers} and obtain that $a=a$ is a set since
-$f(a)=f(a)$ is a set, since $B$ is a groupoid.
-Thus:
-
-\begin{lemma}\label{lem:univ-cover-1type}
-If $f:A\to B$ is a universal \covering and $B$ is a groupoid,
-then $A$ is contractible.
-\end{lemma}
-
-Now assume $(B,b_0)$ is a pointed connected groupoid and $f:A\to B$
-a universal \covering. Since $A$ and $\sum_{b:B}(b_0\eqto_Bb)$ are both
-contractible, and $B$ is connected, we have
-$\Trunc{(A,f)=(\sum_{b:B}(b_0\eqto_Bb),\fst)}$.
-Hence if $(B,b_0)$ is a pointed connected groupoid, all
-universal \coverings can be merely identified with a canonical one.
-Moreover, the type of universal \coverings is equivalent to
-$\bn 1 \to B$, and hence to $B$ itself,
-so the type of \emph{pointed} universal \coverings is contractible.
-This justifies the following definition.
-
-Note that, for a general pointed connected type $(B,b_0)$, we have that
-$(b_0\eqto_B b)$ is a family of \emph{sets} exactly when $B$ is a groupoid.
-The type family $(b_0\eqto_B b)$ is also important if $B$ is not a groupoid,
-but is then not a \emph{set} bundle.\footnote{%
-  Of course, the type $\sum_{b:B}(b_0=b)$ is contractibe
-  by \cref{lem:thepathspaceiscontractible}, for any type $B$.}
-
-\begin{remark}
-  What's so ``universal'' about this?
-The universal \covering over the pointed connected groupoid $(B,b_0)$ coincides with the constant function $\cst{b_0}:\bn 1\to B$ (with value $b_0$), and seems like an unnecessary complicated representation were it not for the manifold practical value of the formulation that we've given.
-In particular, we recognize the set of symmetries $b_0\eqto_Bb_0$ as the preimage of $b_0$ under the first projection from $\uc{b_0}B$ to $B$; ultimately this will show that the study of symmetries coincides with the study of the universal \covering.
-
-The first instance of this comes already in the next section, where we show in \cref{cor:S1groupoid} that the symmetries in the circle are given by the set of integers $\zet$ by showing that the universal \covering and the exponential \covering (\cref{def:RtoS1}) of the circle coincide.
-
-That said, one way to see that the constant function $\cst{b_0}:\bn 1\to B$
-\emph{does} deserve the label universal is the following.\marginnote{%
-  Any $(a_0,p) : f^{-1}(b_0)$ gives rise to a commutative diagram:
-  \[
-    \begin{tikzcd}[column sep=small,ampersand replacement=\&]
-      \bn 1\ar[rr,dashed,"\cst{a_0}"]\ar[dr,"\cst{b_0}"'] \& \& A \ar[dl,"f"] \\
-      \& B \&
-    \end{tikzcd}
-  \]}
-Given any function $f:A\to B$ and $(a_0,p): f^{-1}(b_0)$,
-we get a function $\cst{a_0}:\bn 1\to A$, and $p:b_0=f(a_0)$ gives rise to
-an element in $\cst{b_0}\eqto_{\bn 1\to B}f \circ \cst{a_0}$.
-In other words, any such $f$ is ``a factor of $\cst{b_0}$''.
-Note, however, that this depends on $f^{-1}(b_0)$ being non-empty
-(classically, this is often demanded of a covering, which distinguishes it from our \coverings),
-and the factorization depends on the element $(a_0,p)$ used.
-
-The situation is even simpler for pointed maps:
-For any \emph{pointed} map $f : A \ptdto B$, with $(a_0,f_0):f^{-1}(b_0)$,
-there is a \emph{unique} pointed map $g : \bn 1 \ptdto A$
-(given by the base point of $A$), and this of course also gives
-the unique way to write $f$ as a ``pointed factor of $\cst{b_0}$''.
-\end{remark}
-
-We'll continue the general study of set bundles in \cref{sec:gsets}
+We'll continue the general study of \coverings in \cref{sec:gsets}
 and indeed throughout the book.
-For now, we'll focus our attention on the circle and set bundles over it.
+For now, we'll focus our attention on the circle and \coverings over it.
 
 \section{The symmetries in the circle}
 \label{sec:symcirc}