fix proof of lem:hom-is-set

group.tex

@@ -62,6 +62,8 @@ \section{Brief overview of the chapter}
 \section{The type of groups}
 \label{sec:typegroup}
 
+Recall the definition of pointed types, \cref{def:pointedtypes},
+and the related conventions established in~\cref{sec:pointedtypes}.
 \begin{definition}\label{looptype}
   Given a pointed type $X\jdeq(A,a)$, we define its type of \emph{loops}
   by $\loops X \defeq (a \eqto_A a)$.%
@@ -539,7 +541,7 @@ \subsection{First examples}
 The key insight is provided by the function $R_m:S^1\to\FinSet_m$ from~\cref{def:RmtoS1},
 with $R_m(\base)\defequi\bn m$ and
 $R_m(\Sloop)\defis \zs$, picking out exactly the cyclic permutation
-$\zs:\bn m=\bn m$ (and its iterates) among all permutations.
+$\zs:\bn m\eqto \bn m$ (and its iterates) among all permutations.
 Using our new notation, we can also write this as
 \[
   R_m : \B\ZZ \to \BSG_m.
@@ -562,7 +564,7 @@ \subsection{First examples}
 Since we have a factorization of $R_m$ as the equivalence $c:\Sc\equivto\Cyc_0$
 followed by the map $\blank/m:\Cyc_0 \to \BSG_m$,
 and since $\Cyc_m$ is the $0$-image of the latter by~\cref{thm:image-Z-to-Cm},
-we get a uniquely induced pointed equivalence $g : \BCG'_m \ptdto \BCG_m$.\footnote{%
+we get a uniquely induced pointed equivalence $g : \BCG'_m \ptdweto \BCG_m$.\footnote{%
   More precisely, but using language not yet established: $\CG_m$ is both isomorphic to $\ZZ/m\ZZ$, the ``quotient group'' (\cf \cref{def:normalquotient}) of $\ZZ$ by the ``kernel'' (\cf \cref{def:kernel}) induced by $R_m$, and to $\CG'_m$, which is the corresponding ``image'' (\cf \cref{sec:image}). This pattern will later be captured in~\cref{thm:fund-thm-homs}.}
 This identifies the set $\Trunc{\inv{R_m}(X)}_0$ with the set of cycle structures
   on the $m$-element set $X$.
@@ -932,32 +934,30 @@ \section{Homomorphisms}
 \label{sec:homomorphisms}
 
 \begin{remark}\label{homom-idens}
-Let $G$ and $H$ be groups, and suppose we have a pointed function $f : \BG \ptdto \BH$.
+Let $G$ and $H$ be groups, and suppose we have a pointed function $k : \BG \ptdto \BH$.
 Suppose also, for simplicity (and without loss of generality),
-that $\pt_\BH \jdeq f ( \pt_\BG ) $ and $f_\pt \jdeq \refl{\pt_\BH}$.
-Applying \cref{def:ap} yields a function $F \defeq \ap f : \USymG \to \USymH$, which satisfies the following identities:
+that $\pt_\BH \jdeq k ( \pt_\BG ) $ and $k_\pt \jdeq \refl{\pt_\BH}$.
+Applying \cref{def:ap} yields a function $f \defeq \ap k : \USymG \to \USymH$, which satisfies the following identities:
 \begin{alignat*}2
-  F ( \refl {\pt_\BG} ) & = \refl{\pt_\BH},  &\qquad&                            \\
-  F (g ^ {-1})     & = (F (g))^{-1}         && \text {for any $g : \USymG$},    \\
-  F (g' \cdot g)   & =  F (g') \cdot  F (g) && \text {for any $g, g' : \USymG$}.
+  f ( \refl {\pt_\BG} ) & = \refl{\pt_\BH},  &\qquad&                            \\
+  f (g ^ {-1})     & = (f (g))^{-1}         && \text {for any $g : \USymG$},    \\
+  f (g' \cdot g)   & =  f (g') \cdot  f (g) && \text {for any $g, g' : \USymG$}.
 \end{alignat*}
 The first one is true by definition, the second can be proved by induction on $g$, and the third one follows from \cref{lem:apcomp}.
-These three identities assert that the function $\ap f$ \emph{preserves}, in a certain sense, the operations provided by \cref{lem:idtypesgiveabstractgroups} that
+These three identities assert that the function $\ap k$ \emph{preserves}, in a certain sense, the operations provided by \cref{lem:idtypesgiveabstractgroups} that
 make up the abstract groups $\abstr(G)$ and $\abstr(H)$.
-In the traditional study of abstract groups, these three identities play an important role and entitle one to call the function $F$ a
+In the traditional study of abstract groups, these three identities play an important role and entitle one to call the function $f$ a
 \emph{homomorphism of abstract groups}.\index{homomorphism}
 \end{remark}
 
 A slight generalization of the discussion above will be to suppose that we have a general pointed map with an arbitrary witness of pointedness
-$f_\pt : \pt_\BH \eqto f ( \pt_\BG ) $,
+$k_\pt : \pt_\BH \eqto k ( \pt_\BG ) $,
 not necessarily given by reflexivity.  Indeed, that works out, thereby motivating the following definition.
 
 \begin{definition}\label{def:grouphomomorphism}
   The type of \emph{group homomorphisms}\index{homomorphism!of groups}
   from $G:\typegroup$ to
   $H:\typegroup$ is defined to be\marginnote{%
-    % Sometimes we write $f : G\to_\Group H$ instead of $f : \Hom(G,H)$
-    % to emphasize that $f$ is a map of groups.
     When it is clear from context that a homomorphism is intended,
     we may write $f : G \to H$.}
   \[
@@ -985,29 +985,31 @@ \section{Homomorphisms}
       .. controls ++(270:-1.5) and ++(80:1.4)  .. (-1,1)
       .. controls ++(80:-1.4)  and ++(170:1) .. (0,-1);
       \node[dot,label=left:$\pt_Y$] (a) at (0,0) {};
-      \node[dot,label=below:$f(\pt_X)$] (b) at (1.5,-.5) {};
-      \node (ct) at (2.6,1.1) {$\ap{f_\div}(p)$};
-      \draw[->] (a) .. controls ++(-20:1) and ++(170:1) .. node[auto,swap] {$f_\pt$} (b);
+      \node[dot,label=below:$k(\pt_X)$] (b) at (1.5,-.5) {};
+      \node (ct) at (2.6,1.1) {$\ap{k_\div}(p)$};
+      \draw[->] (a) .. controls ++(-20:1) and ++(170:1) .. node[auto,swap] {$k_\pt$} (b);
       \draw[->] (b) .. controls ++(20:1) and ++(-40:1) ..
       (2,1) .. controls ++(-40:-1) and ++(-80:-1) .. (b);
     \end{tikzpicture}}
 
 \begin{definition}\label{def:loops-map}
-  Given pointed types $X$ and $Y$ and a pointed function $f : X\ptdto Y$ (as defined in \cref{def:pointedtypes}),
-  we define a function $\loops f : \loops X \to \loops Y$ by setting\footnote{%
-    Recall~\cref{def:ap} for $\ap{}$.}
+  Given pointed types $X$ and $Y$ and a pointed function $k : X\ptdto Y$ (as defined in \cref{def:pointedtypes}),
+  we define a function $\loops k : \loops X \to \loops Y$ by setting\footnote{%
+    Recall~\cref{def:ap} for $\ap{}$.
+    Note also that $\loops k$ is pointed: we can identify $\loops k(\refl{\pt_X})$
+  with $\refl{\pt_Y}$.}
   \[
-    \loops f(p) \defeq f_\pt^{-1} \cdot \ap{f_\div}(p) \cdot f_\pt.\qedhere
+    \loops k(p) \defeq k_\pt^{-1} \cdot \ap{k_\div}(p) \cdot k_\pt.\qedhere
   \]
 \end{definition}
 
 \begin{remark}\label{rem:loops-map}
-  If $f : X \ptdto Y$ has the reflexivity path $\refl{Y_\pt}$ as its witness
-  of pointedness, then we have an identification $\loops f \eqto \ap{f_\div}$.
+  If $k : X \ptdto Y$ has the reflexivity path $\refl{Y_\pt}$ as its witness
+  of pointedness, then we have an identification $\loops k \eqto \ap{k_\div}$.
 \end{remark}
 
 \begin{definition}\label{def:USym-hom}
-  Given groups $G$ and $H$ and a homomorphism  $f$ from $G$ to, we define a function $\USymf : \USymG \to \USymH$
+  Given groups $G$ and $H$ and a homomorphism  $f$ from $G$ to $H$, we define a function $\USymf : \USymG \to \USymH$
   by setting $\USymf \defeq \loops \Bf$.
   In other words, the homomorphism $\mkhom\Bf$
   induces $\loops\Bf$ as the map on underlying symmetries.
@@ -1048,8 +1050,11 @@ \section{Homomorphisms}
   \[
     (G\eqto_\typegroup G')\equivto \Iso(G,G')
   \]
-  between the identity type between the groups $G$ and $G'$ and the set of isomorphisms,
-  and we continue using the notation $\ptoe p$ from \cref{def:idtoeq} for the equivalence corresponding to an identification $p:G\eqto G'$.
+  between the identity type between the groups $G$ and $G'$ and the set of isomorphisms.
+  We allow ourselves to also write $p : \Iso(G,G')$ for the isomorphism
+  corresponding to an identification $p:G\eqto G'$,
+  and $\Bp : \BG \ptdweto \BG'$ for the corresponding pointed equivalence
+  of classifying types.
 \end{remark}
 
 
@@ -1071,18 +1076,20 @@ \section{Homomorphisms}
     applied to homomorphisms as we do for groups.}
 \end{remark}
 
-  Identifications of homomorphisms $f\eqto_{\Hom(G,H)}h$\marginnote{\wip{I
-      guess we can't use $=$ until we prove that $\Hom(G,H)$
-      is indeed a set?}}
-  are equivalent to identifications of pointed maps
-  $\Bf \eqto_{\BG\ptdto\BH} \Bh$;
-  the latter are (by \cref{lem:isEq-pair=}) given by
-  pairs of an identification of (unpointed) maps
-  $H : \Bf_\div \eqto_{(\BG_\div \to \BH_\div)} \Bh_\div$ with an identification\marginnote{%
-    \wip{picture!}}
-  \[
-    K : H(\shape_G)\Bf_\pt \eqto_{(\shape_H \eqto \Bh_\div(\shape_G))} \Bh_\pt.\qedhere
-  \]
+Identifications of homomorphisms $f\eqto_{\Hom(G,H)}f'$
+are equivalent to identifications of pointed maps
+$\Bf \eqto_{\BG\ptdto\BH} \Bf'$;
+the latter are
+(by \cref{lem:isEq-pair=} and the fact that $\BH$ is a groupoid)
+given by identifications of (unpointed) maps
+$H : \Bf_\div \eqto_{(\BG_\div \to \BH_\div)} \Bf'_\div$ such that\marginnote{%
+  \begin{tikzcd}[ampersand replacement=\&,column sep=small]
+    \& \shape_H\ar[dl,eql,"{\Bf_\pt}"'] \ar[dr,eqr,"\Bf'_\pt"] \& \\
+    \Bf_\div(\shape_G) \ar[rr,eql,"{H(\shape_G)}"'] \& \& Bf'_\div(\shape_G)
+  \end{tikzcd}}
+\[
+  H(\shape_G)\Bf_\pt = \Bf'_\pt.
+\]
 
 We will later show that if $G$ and $H$ are groups, then $\Hom(G,H)$
 is equivalent to the \emph{set} of ``abstract group homomorphisms''
@@ -1093,64 +1100,20 @@ \section{Homomorphisms}
   is a set for all groups $G,H$.
 \end{lemma}
 \begin{proof}
-  but it is instructive to prove that $\Hom(G,H)$, or equivalently
+  Given homomorphisms $f,f':\Hom(G,H)$, we use the equivalence just
+  described,
   \[
-    (\BG\ptdto\BH) \defequi
-    \sum_{F:\BG_\div\to \BH_\div}(\shape_H=F(\shape_G)),
+    (f \eqto f') \equivto \sum_{H:\Bf_\div\eqto\Bf'_\div}
+    H(\shape_G)\Bf_\pt = \Bf'_\pt,
   \]
-  is a set directly from the definition. Recall our notation: a
-  homomorphism $f:\Hom(G,H)$ is recorded as the pair
-  \begin{displaymath}
-    \Bf \jdeq (\Bf_\div,p_f):\sum_{F:\BG_\div\to \BH_\div}(\shape_H=F(\shape_G)).
-  \end{displaymath}
-  Let us spell out the data needed to give an identity between two
-  group homomorphisms $f,f':\Hom(G,H)$.  We clearly must have a
-  $$J:\Bf_\div=\Bf_\div',$$
-  which by function extensionality (\cref{def:funext}) is equivalently
-  given by its image given by the element (with the same
-  name) in the $\Pi$-type
-  $$J:\prod_{z:\BG_\div}\Bf_\div(z)=\Bf'_\div(z).$$
-   \marginnote{  \begin{displaymath}
-    \xymatrix{&\shape_H\ar@{=}[dl]_{p_f}^{\rotatebox{35}{\footnotesize$\gets$}}
-      \ar@{=}[dr]^{p_{f'}}_{\rotatebox{-35}{\footnotesize$\to$}}&\\
-      \Bf_\div(\shape_G)\ar@{=}[rr]^{J(\shape_G)}_\to&&\,\Bf'_\div(\shape_G).}
-  \end{displaymath}}
-Transport along $J$ of $p_f:\shape_H=\Bf_\div(\shape_G)$ shows that in
-  addition we must have a path $!:J(\shape_G)\cdot p_f=p_{f'}$
- in the
-  type ${\shape_H=\Bf'_\div(\shape_G)}$.
-  In other words, we have an equivalence
-  $$(f=f')\simeq \sum_{J:\Bf_\div=\Bf'_\div}J(\shape_G)p_f=p_{f'},$$
-  and our goal is to prove that any two elements are identical.
-  \marginnote{Induction on $\gamma:\shape_G=z$ gives
-   $$\xymatrix{
-    \Bf_\div(\shape_G)\ar@{=}[rr]^{J(\shape_G)}_\to\ar@{=}[d]^\downarrow_{\Bf_\div(\gamma)}&&
-    \Bf'_\div(\shape_G)\ar@{=}[d]^\downarrow_{\Bf'_\div(\gamma)}\\
-    \Bf_\div(z)\ar@{=}[rr]^{J(z)}_\to&&\,\Bf'_\div(z).}
-  $$
-  Together these two commutative diagrams (and the fact that we're in a set) show that $(J,!)$ is unique.}
-   Take two elements $(J,!),(K,!):\sum_{J:\Bf_\div=\Bf'_\div}J(\shape_G)p_f=p_{f'}$.  We must prove that $(J,!) = (K,!)$ has
-   an element.
-  % Notice that, for any $L:\Bf_\div = \Bf'_\div$, one can
-  % prove by induction on $\gamma:\shape_G=x$ that the following diagram
-  % commutes:
-  % $$\xymatrix{
-  %   \Bf_\div(\shape_G)\ar@{=}[r]^{L(\shape_G)}_\to\ar@{=}[d]^\downarrow_{\Bf_\div(\gamma)}&
-  %   \Bf'_\div(\shape_G)\ar@{=}[d]^\downarrow_{\Bf'_\div(\gamma)}\\
-  %   \Bf_\div(z)\ar@{=}[r]^{L(z)}_\to&\,\Bf'_\div(z).}
-  % $$
-  % It means in particular that, for propositional goals, $L$ is
-  % entirely determined by $L(\shape_G)$. More precisely, the remark
-  % applies to $J$ and $K$ when we try to prove $(J,!) = (K,!)$.
-  Indeed,
-  this type is equivalent to $J=K$, which is in turn equivalent to
-  $\prod_{z:\BG_\div}J(z)=K(z)$, and because $\Bf_\div(z)=\Bf'_\div(z)$
-  is a set for every $z$ ($\BH_\div$ being a groupoid), the type
-  $J(z)=K(z)$ is a proposition. Hence, with the propositional goal
-  $(J,!) = (K,!)$, one can now use connectedness of $\BG_\div$, and
-  only check the equality on the point $\shape_G$. By definition,
+  so our goal is to prove that any two elements $(H,!),(J,!)$ of the right-hand side
+  can be identified.
+  By function extensionality, the type $H\eqto J$ is equivalent to
+  the proposition $\prod_{t:\BG_\div} H(t) = J(t)$. So now we can use
+  connectedness of $\BG_\div$, and
+  only check the equality on the point $\shape_G$. By assumption,
   \begin{displaymath}
-    J(\shape_G) = p_{f'}\inv{p_f} = K(\shape_G).
+    H(\shape_G) = \Bf'_\pt \inv{\Bf_\pt} = J(\shape_G).
   \end{displaymath}
   This concludes the proof that $f=f'$ is a proposition, or in other
   words that $\Hom(G,H)$ is a set.
@@ -2725,7 +2688,7 @@ \section{Abelian groups}
 $\BG_\div\simeq \BG_\div$ as the operator ``$\weq$'' acts on bare
 types. To refer to the type of pointed equivalences (that is the
 pointed functions whose underlying functions are equivalences), we
-shall use the notation $\BG \ptdweq \BG$.%
+shall use the notation $\BG \ptdweto \BG$.%
 
 \subsection{Center of a group}
 \label{sec:center-group}
@@ -3231,11 +3194,11 @@ \subsection{Abelian groups and simply connected $2$-types}
   (\cref{def:abelian-groups}), and so it yields an element of
   $\loopspace {(\BB G)} \eqto_{\typegroup} G$. %
   \marginnote[-1.5\baselineskip]{%
-    If $X \ptdweq Y$ denote the type of pointed equivalences between
+    If $X \ptdweto Y$ denote the type of pointed equivalences between
     pointed types $X,Y:\UUp$, then the univalence axiom implies that
     there is an equivalence
     \begin{displaymath}
-      (X=Y) \weq (X \ptdweq Y).
+      (X=Y) \weq (X \ptdweto Y).
     \end{displaymath}%
   }%
   Conversely, take a pointed simply connected $2$-type $(A,a)$. We

intro-uf.tex

@@ -3350,7 +3350,7 @@ \section{Pointed types}\label{sec:pointedtypes}
   If $X$ and $Y$ are pointed types, we define the type of pointed equivalences
   from $X$ to $Y$ as:
   \[
-    X \ptdweq Y \defeq \sum_{f : X \ptdto Y}\isEq(f_\div)\qedhere
+    X \ptdweto Y \defeq \sum_{f : X \ptdto Y}\isEq(f_\div)\qedhere
   \]
 \end{definition}
 \begin{xca}\label{xca:pointedequiv}
@@ -3359,7 +3359,7 @@ \section{Pointed types}\label{sec:pointedtypes}
   as well as an identification $q : \pt_Y \eqto \ptoe p_\div(\pt_X)$.
   Together, this gives a map of type
   \[
-    (X \eqto Y) \to (X \ptdweq Y).
+    (X \eqto Y) \to (X \ptdweto Y).
   \]
   Show that this is an equivalence.
 \end{xca}

macros.tex

@@ -808,7 +808,7 @@
 \newcommand*{\inv}[1]{#1^{-1}}%
 %% \newcommand*{\invo}[1]{#1^{-1\mathop{\constant{o}}}}%mathop deliberately to center the o
 \newcommand*{\ptdto}{\to_\ast}%
-\newcommand*{\ptdweq}{\equivto_\ast}%
+\newcommand*{\ptdweto}{\equivto_\ast}%
 \newcommand*{\mono}{\hookrightarrow}%
 \newcommand*{\epi}{\twoheadrightarrow}%
 \newcommand*{\loops}[1][\null]{\Omega^{#1}} % no space