wip Construction 12.1.16

Author: Marc Bezem

fields.tex

@@ -305,19 +305,19 @@ \subsection{Move to a better place (Ch.\ 11 or 2)}
 Let $A$ and $B$ be pointed types and 
 let $f: A\ptdto B$ be a pointed map.
 Then we have an identification of $O(f)\circ \ev_A$ 
-and $\ev_B \circ {\loops(f)}$, as represented by \cref{fig:Omega-O}.
-Consequently, we have that $e\defeq(\inv{\ev_B}\circ{{\blank}\circ\ev_A})$
-is a pointed equivalence of type 
+and ${\ev_B} \circ {\loops(f)}$, as represented by \cref{fig:Omega-O}.
+Consequently, we have that $e\defeq(\ev_B\circ{{\blank}\circ\inv{\ev_A}})$
+is an equivalence of type 
 $(\loops A\ptdto\loops B)\equivto(\Sc A\ptdto\Sc B)$
 with $O \eqto (e\circ \loops)$. 
 \end{construction}
 \begin{implementation}{con:Omega-O}
 Elaborating the situation in \cref{fig:Omega-O}, we have to
-identify (1) and (2) for all $(p,p_\pt)$ by a map $e$ and
+identify (1) and (2) for all $(p,p_\pt)$ by a map $i$ and
 give an identification to fill the following diagram: 
 
 \begin{tikzcd}[ampersand replacement=\&]
-  \& \&\inv{f_\pt}\cdot f(\cst{\pt_A}(\Sloop)\cdot \refl{})\cdot f_\pt  \ar[dddd,eqr,"{e(\cst{\pt_A},\refl{\pt_A})}"]
+  \& \&\inv{f_\pt}\cdot f(\cst{\pt_A}(\Sloop)\cdot \refl{})\cdot f_\pt  \ar[dddd,eqr,"{i(\cst{\pt_A},\refl{\pt_A})}"]
 \\
   \&\loops(f)(\refl{\pt_A})
    \ar[ru,eqr,"{\loops(f)((\ev_A)_\pt)}"]