diff --git a/group.tex b/group.tex index 902ccb4..c525416 100644 --- a/group.tex +++ b/group.tex @@ -2417,14 +2417,14 @@ \section{Homomorphisms; abstract vs.~concrete} $$ and so, since $\iscontr~C(x)$ is a proposition $$ - \prod_{x:\BG_\div}~ \Trunc{a = x}\rightarrow\iscontr~ C(x) + \prod_{x:\BG_\div}~ \Trunc{{\shape_G} = x}\rightarrow\iscontr~ C(x) $$ Since $\BG_\div$ is connected, we have $\prod_{x:\BG_\div}\iscontr~ C(x)$ and so, in particular, we have an element of $\prod_{x:\BG_\div}C(x)$. We get in this way a map $g:\BG_\div\rightarrow \BH_\div$ - together with a map $p:(a=x)\rightarrow ({\shape_H} = g(x))$ such that + together with a map $p:({\shape_G}=x)\rightarrow ({\shape_H} = g(x))$ such that $p (\alpha\omega) = p(\alpha) f(\omega)$ for all $\alpha$ in ${\shape_G}=x$ and $\omega$ in ${\shape_G}={\shape_G}$. We have, for $\alpha:{\shape_G}=x$