symmetry.tex

% Commented out BID 211116 \section{Cayley diagram}
% \label{sec:cayley-diagram}

% We have seen in the previous chapter how cyclic groups
% (those generated by a single generator)
% have neatly described torsors.

% In this section we shall generalize this story
% to groups $G$ generated by a
% (finite or just decidable)
% set of generators $S$.

% \tikzset{vertex/.style={circle,fill=black,inner sep=0pt,minimum size=4pt}}
% \tikzset{gena/.style={draw=casblue,-stealth}}
% \tikzset{genb/.style={draw=casred,-stealth}}

% \begin{figure}
%   \begin{sidecaption}%
%     {Cayley diagram for $S_3$ with respect to $S = \{(12),(23)\}$.}[fig:cayley-s3]
%   \centering
%   \begin{tikzpicture}
%     \pgfmathsetmacro{\len}{2}
%     \node[vertex,label=30:$(13)$]   (n13)  at (30:\len)  {};
%     \node[vertex,label=90:$(132)$]  (n132) at (90:\len)  {};
%     \node[vertex,label=150:$(12)$]  (n12)  at (150:\len) {};
%     \node[vertex,label=210:$e$]     (ne)   at (210:\len) {};
%     \node[vertex,label=270:$(23)$]  (n23)  at (270:\len) {};
%     \node[vertex,label=330:$(123)$] (n123) at (330:\len) {};
%     \begin{scope}[every to/.style={bend left=22}]
%       % generator a is (12)
%       \draw[gena] (ne)   to (n12);
%       \draw[gena] (n12)  to (ne);
%       \draw[gena] (n13)  to (n132);
%       \draw[gena] (n132) to (n13);
%       \draw[gena] (n123) to (n23);
%       \draw[gena] (n23)  to (n123);
%       % generator b is (23)
%       \draw[genb] (ne)   to (n23);
%       \draw[genb] (n23)  to (ne);
%       \draw[genb] (n13)  to (n123);
%       \draw[genb] (n123) to (n13);
%       \draw[genb] (n12)  to (n132);
%       \draw[genb] (n132) to (n12);
%     \end{scope}
%   \end{tikzpicture}
%   \end{sidecaption}
% \end{figure}

% $G \equiv \Aut(D_G) \to \Sym(\Card G)$

% \section{Actions}
% MOVED TO G-SETS BID 211116
% \label{sec:actions}

% \begin{definition}\label{action}
%   If $G$ is any (possibly higher) group and $A$ is any type of objects,
%   then we define an \emph{action} by $G$ in the world of elements of $A$ as a function
%   \[
%     X : \BG \to A.\qedhere
%   \]
% \end{definition}

% The particular object of type $A$ being acted on is $X(\pt):A$,
% and the action itself is given by transport.
% This generalizes our earlier definition of $G$-sets, $X : \BG \to \Set$.

% \begin{definition}\label{std-action}
%   The \emph{standard action} of $G$ on its designated shape $\shape_G$ is obtained by
%   taking $A \defeq \B G$ and $X \defeq \id_{\B G}$.
% \end{definition}

% \begin{example}
%   An action of $G$ on its set $\USymG$ of symmetries is provided by taking $X$ to be the principal torsor $\princ G$ as defined in
%   \cref{def:principaltorsor}.
% \end{example}

% Notice that the type $\BG \to A$ is equivalent to the type
% \[
%   \sum_{a:A}\hom(G,\Aut_A(a)),
% \]
% that is, the type of pairs of an element $a : A$,
% and a homomorphism from $G$ to the automorphism group of $A$.
% The equivalence maps $X:\BG\to A$ to the pair consisting of $X(\pt)$
% and the homomorphism represented by the pointed map arising
% from corestricting $X$ to factor through the component of $A$ containing $a$
% together with the trivial proof that this map takes $\pt:\BG$ to $a$.

% Because of this equivalence,
% we define a \emph{$G$-action on $a:A$}
% to be a homomorphism from $G$ to $\Aut_A(a)$.

% Many times we are particularly interested in actions on types,
% i.e., $A$ is a universe (or the universe of types-at-large):
% \[
%   X : \BG \to \UU.
% \]

% In this case, we define \emph{orbit type} of the action as
% \[
%   X_G \defeq \sum_{z:\BG} X(z),
% \]
% and the type of \emph{fixed points} as
% \[
%   X^G \defeq \prod_{z:\BG} X(z).
% \]
% The set of orbits is the set-truncation of the orbit type,
% \[
%   X / G \defeq \Trunc{X_G}_0.
% \]
% We say that the action is \emph{transitive} if $X / G$ is contractible.

% \section{Heaps \texorpdfstring{$(\dagger)$}{(\textdagger)}}
% \label{sec:heaps}

% Recall that we in \cref{rem:heap-preview} wondered about
% the status of general identity types $a=_A a'$,
% for $a$ and $a'$ elements of a groupoid $A$,
% as opposed to the more special loop types $a=_Aa$.\marginnote{%
%   This section has no implications for the rest of the book,
%   and can thus safely be skipped on a first reading.
%   (TODO: Move in place in \cref{ch:groups}?)}
% Here we describe the resulting algebraic structure
% and how it relates to groups.

% We proceed in a fashion entirely analogous to that of \cref{sec:typegroup},
% but instead of looking a pointed types, we look at \emph{bipointed types}.

% \begin{definition}\label{def:bipt-conn-groupoid}
%   The type of \emph{bipointed, connected groupoids} is the type
%   \[
%     \UUppone \defeq \sum_{A:\UU^{=1}}(A \times A).\qedhere
%   \]
% \end{definition}
% Recall that $\UU^{=1}$ is the type of connected groupoids $A$,
% and that we also write $A:\UU$ for the underlying type.
% We write $(A,a,a'):\UUppone$ to indicate the two endpoints.

% Analogous to the loop type of a pointed type,
% we have a designated identity type of a bipointed type,
% where we use the two points as the endpoints of the identifications:
% We set $\ISym(A,a,a') \defeq (a =_A a')$.

% \needspace{6\baselineskip}
% \begin{definition}\label{def:heap}
%   The type of \emph{heaps}\footnote{%
%     The concept of heap (in the abelian case)
%     was first introduced by Prüfer\footnotemark{}
%     under the German name \emph{Schar} (swarm/flock).
%     In Anton Sushkevich's book
%     \casrus{Теория Обобщенных Групп}
%     (\emph{Theory of Generalized Groups}, 1937),
%     the Russian term \casrus{груда} (heap)
%     is used in contrast to \casrus{группа} (group).
%     For this reason, a heap is sometimes
%     known as a ``groud'' in English.}%
%   \footcitetext{Pruefer-AG}
%   is a wrapped copy (\cf \cref{sec:unary-sum-types})
%   of the type of bipointed, connected groupoids $\UUppone$,
%   \[
%     \Heap \defeq \Copy_{\mkheap}(\UUppone),
%   \]
%   with constructor $\mkheap : \UUppone \to \Heap$.
% \end{definition}
% We call the destructor $\B : \Heap \to \UUppone$,
% and call $\BH$ the \emph{classifying type} of the heap $H \jdeq\mkheap\BH$,
% just as for groups,
% and we call the first point in $BH$ is \emph{start shape} of $H$,
% and the second point the \emph{end shape} of $H$.

% The identity type construction $\ISym : \UUppone \to \Set$
% induces a map $\USym : \Heap \to \Set$,
% mapping $\mkheap X$ to $\ISym X$.
% These are the \emph{underlying identifications} of the heaps.

% These is an obvious map (indeed a functor) from groups to heaps,
% given by doubling the point.
% That is, we keep the classifying type and use the designated shape
% as both start and end shape of the heap.
% In fact, this map lifts to the type of heaps with a chosen identification.
% \begin{exercise}\label{xca:group+torsor-heap}
%   Define natural equivalences $\Heap \weq \sum_{G:\Group}\BG$,
%   and $\Group \weq \sum_{H:\Heap}(\USymH)$.
% \end{exercise}
% Recalling the equivalence between $\BG$ and the type of $G$-torsors
% from~\cref{lem:BGbytorsor},
% we can also say that a heap is the same
% as a group $G$ together with a $G$-torsor.\footnote{%
%   But be aware that are \emph{two} such descriptions,
%   according to which endpoint is the designated shape,
%   and which is the ``twisted'' torsor.}
% It also follows that the type of heaps is a (large) groupoid.

% In the other direction,
% there are \emph{two} obvious maps (functors) from heaps to groups,
% taking either the start or the end shape to be the designated shape.

% Here's an \emph{a priori} different map from heaps to groups:
% For a heap $H$, consider all the
% symmetries of the underlying set of identifications $\USymH$
% that arise as $r \mapsto p\inv q r$ for $p,q\in \USymH$.

% Note that $(p,q)$ and $(p',q')$ determine the same symmetry
% if and only if $p\inv q = p'\inv{q'}$, and if and only if
% $\inv{p'}p = \inv{q'}q$.

% For the composition, we have $(p,q)(p',q') = (p\inv{q}p',q') = (p,q'\inv{p'}q)$.

% \begin{exercise}
%   Complete the argument that this defines a map
%   from heaps to groups. Can you identify the resulting group
%   with the symmetry group of the start or end shape?
%   How would you change the construction to get the other endpoint?
% \end{exercise}

% \begin{exercise}
%   Show that the symmetry groups of the two endpoints of a heap
%   are \emph{merely} isomorphic.

%   Define the notion of an \emph{abelian heap},
%   and show that for abelian heaps,
%   the symmetry groups of the endpoints are (\emph{purely}) isomorphic.
% \end{exercise}

% Now we come to the question of describing the algebraic structure
% of a heap.
% Whereas for groups we can define the abstract structure
% in terms of the reflexivity path and the binary operation of path composition,
% for heaps, we can define the abstract structure
% in terms of a \emph{ternary operation},
% as envisioned by the following exercise.

% \begin{exercise}\label{xca:heap-variety}
%   Fix a set $S$.
%   Show that the fiber $\inv{\USym}(S)\jdeq\sum_{H:\Heap}(S=\USymH)$ is a set.

%   Now fix in addition a ternary operation $t:S\times S\times S\to S$ on $S$.
%   Show that the fiber of the map $\Heap \to \sum_{S:\Set}(S\times S\times S \to S)$,
%   mapping $H$ to $(\USymH,(p,q,r)\mapsto p \inv{q} r)$,
%   at $(S,t)$ is a proposition,
%   and describe this proposition in terms of equations.
% \end{exercise}

% \section{Semidirect products}
% \label{sec:Semidirect-products}

% In this section we describe a generalization of the product of two group, called the {\em semidirect} product, which can be constructed from an
% action of a group on a group.  Like the product, it consists of pairs, both at the level of concrete groups and of abstract groups, as we shall
% see.

% We start with some preliminaries on paths between pairs.
% Lemma \cref{lem:isEq-pair=} above takes a simpler form when $y$ and $y'$ are values of a family $x \mapsto f(x)$
% of elements of the family $x \mapsto Y(x)$, as the following lemma shows.

% \begin{lemma}\label{lem:pathpairsection}
%   Suppose we are given a type $X$ and a family of types $Y(x)$ parametrized by the elements $x$ of $X$.
%   Suppose we are also given a function $f : \prod_{x:X} Y(x)$.
%   For any elements $x$ and $x'$ of $X$,
%   there is an equivalence of type
%   $$\left ( (x,f(x)) = (x',f(x')) \right ) \weq (x=x') \times (f(x) = f(x)),$$
%   where the identity type on the left side is between elements of $\sum_{x:X} Y(x)$.
% \end{lemma}

% \begin{proof}
%   By \cref{lem:isEq-pair=} and by composition of equivalences, it suffices to establish an equivalence of type
%   $$\left( \sum_{p:x=x'} \pathover {f(x)} Y p {f(x')} \right) \weq (x=x') \times (f(x) = f(x)).$$
%   Rewriting the right hand side as a sum over a constant family, it suffices to find an equivalence of type
%   $$\left( \sum_{p:x=x'} \pathover {f(x)} Y p {f(x')} \right) \weq \sum_{p:x=x'} (f(x) = f(x)).$$
%   By \cref{lem:fiberwise} it suffices to establish an equivalence of type
%   $$ \left( \pathover {f(x)} Y p {f(x')} \right) \weq (f(x) = f(x))$$
%   for each $p:x=x'$.  By induction on $x'$ and $p$ we reduce to the case where $x'$ is $x$ and $p$ is $\refl x$, and it suffices to establish an
%   equivalence of type
%   $$ \left( \pathover {f(x)} Y {\refl x} {f(x)} \right) \weq (f(x) = f(x)).$$
%   Now the two sides are equal by definition, so the identity equivalence provides what we need.
% \end{proof}

% The lemma above shows how to rewrite certain paths between pairs as pairs of paths.  Now we wish to establish the formula for composition of
% paths, rewritten in terms of pairs of paths, but first we introduce a convenient definition for the transport of loops in $Y(x)$ along paths in
% $X$.

% \begin{definition}\label{def:pathsectionaction}
%   Suppose we are given a type $X$ and a family of types $Y(x)$ parametrized by the elements $x$ of $X$.
%   Suppose we are also given a function $f : \prod_{x:X} Y(x)$.
%   For any elements $x$ and $x'$ of $X$ and for any identity $p : x = x'$, define a function $(f(x') = f(x')) \to (f(x) = f(x))$, to be denoted
%   by $q' \mapsto {q'} ^ p$, by induction on $p$ and $x'$, reducing to the case where $x'$ is $x$ and $p$ is $\refl x$, allowing us to
%   set ${q'} ^{ \refl x } \defeq q'$.
% \end{definition}

% We turn now to associativity for the operation just defined.

% \begin{lemma}\label{def:pathsectionactionassoc}
%   Suppose we are given a type $X$ and a family of types $Y(x)$ parametrized by the elements $x$ of $X$.
%   Suppose we are also given a function $f : \prod_{x:X} Y(x)$.
%   For any elements $x$, $x'$, and $x''$ of $X$, for any identities $p : x = x'$ and $p' : x' = x''$,
%   and for any $q : f x'' = f x''$,
%   there is an identification of type $ ( q ^{ p' }) ^ p = q ^{( p' \cdot p )}$.
% \end{lemma}

% \begin{proof}
%   By induction on $p$ and $p'$, it suffices to show that $ ( q ^{ \refl y }) ^ { \refl y } = q ^{( \refl y \cdot \refl y )}$, in which both sides are
%   equal to $q$ by definition.
% \end{proof}

% Observe that the operation depends on $f$, but $f$ is not included as part of the notation.

% The next lemma contains the formula we are seeking.

% \begin{lemma}\label{lem:pathpairsectionmult}
%   Suppose we are given a type $X$ and a family of types $Y(x)$ parametrized by the elements $x$ of $X$.
%   Suppose we are also given a function $f : \prod_{x:X} Y(x)$.
%   For any elements $x$, $x'$, and $x''$ of $X$, and for any two identities $e : (x,f(x)) = (x',f(x'))$ and $e' : (x',f(x')) = (x'',f(x''))$,
%   if $e$ corresponds to the pair $(p,q)$ with $p : x = x'$ and $q : f x = f x$ under the equivalence of \cref{lem:pathpairsection},
%   and $e'$ corresponds to the pair $(p',q')$ with $p' : x' = x''$ and $q' : f x' = f x'$,
%   then $e' \cdot e$ corresponds to the pair $(p' \cdot p , ({q'} ^ p) \cdot q)$.
% \end{lemma}

% \begin{proof}
%   By induction on $p$ and $p'$ we reduce to the case where $x'$ and $x''$ are $x$ and $p$ and $p'$ are $\refl x$.
%   It now suffices to show that $e' \cdot e$ corresponds to the pair $(\refl x , q' \cdot q)$.
%   Applying the definition of the map $\Phi$ in the proof of \cref{lem:isEq-pair=} to our three pairs, we see that it suffices to show that
%   $\left( \apap g {\refl x} {q'} \right) \cdot \left( \apap g {\refl x} {q} \right) = \apap g {\refl x} {q' \cdot q}$, with $g$, as there, being the function $ g(x)(y) \defeq (x,y)$.
%   By \cref{def:applfun2comp} it suffices to show that $\left( \ap {g(x)} {q'} \right) \cdot \left( \ap {g(x)} {q} \right) = \ap {g(x)} {(q' \cdot q)}$, which follows from
%   compatibility of $\ap {g(x)}$ with composition, as in \cref{lem:apcomp}.
% \end{proof}

% The lemma above will be applied mostly in the case where $x'$ and $x''$ are $x$, but if it had been stated only for that case, we would not have
% been able to argue by induction on $p$ and $p'$.

% \begin{definition}\label{def:semidirect-product}
%   Given a group $G$ and an action $\tilde H : \BG \to \typegroup$ on a group $H \defeq \tilde H(\shape_G)$, we define a group called the {\em
%     semidirect product} as follows.
%   $$G \ltimes \tilde H \defeq \mkgroup { \sum_{t:\BG} \B \tilde H(t) }$$
%   Here the basepoint of the sum is taken to be the point $(\shape_G,\shape_H)$.
%   (We deduce from \cref{lem:level-n-utils}, \cref{level-n-utils-sum}, that $\sum_{t:\BG} \B \tilde H(t)$ is a groupoid.
%   See \cref{lem:UNKNOWN} for a proof that $\sum_{t:\BG} \B \tilde H(t)$ is connected.)
% \end{definition}

% Observe that if the action of $G$ on $H$ is trivial, then $\tilde H(t) \jdeq H$ for all $t$ and $G \ltimes \tilde H \jdeq G \times H$.

% Projection onto the first factor gives a homomorphism $p \defeq \mkgroup \fst : G \ltimes \tilde H \to G$.
% Moreover, there is a homomorphism $s : G \to G \ltimes \tilde H$ defined by
% $ s \defeq \mkgroup {\left( t \mapsto (t,\shape_{\tilde H(t)}) \right) }$, for $t : \B G$.
% The two maps are homomorphisms because they are made from basepoint-preserving maps.
% The map $s$ is a \emph{section} of $p$ in the sense the $p \circ s = \id_G$.
% There is also a homomorphism $j : H \to G \ltimes \tilde H$ defined by $j \defeq \mkgroup { \left( u \mapsto (\shape_G,u) \right) }$, for $u : \B H$.

% \begin{lemma}
%   The homomorphism $j$ above is a monomorphism, and it gives the same (normal) subgroup of $G \ltimes \tilde H$ as the kernel $\ker p$ of $p$.
% \end{lemma}

% \begin{proof}
%   See \ref{def:kernel} for the definition of kernel.  According to \cref{lem:fst-fiber(a)=B(a)}, the map $\B H \to (\B p)^{-1}(\shape_G)$ defined by
%   $ u \mapsto ((\shape_G,u), \refl{\shape_G}) $ is an equivalence.  This establishes that the fiber $(\B p)^{-1}(\shape_G)$ is connected and thus serves as
%   the classifying type of $\ker p$.  Pointing out that the composite map $H \xrightarrow{\isom} \ker p \to G \ltimes \tilde H$ is $j$ and using
%   univalence to promote the equivalence to an identity gives the result.
% \end{proof}

% Our next goal is to present the explicit formula for the multiplication operation in $\USym { G \ltimes \tilde H }$.
% First we apply \cref{lem:pathpairsection} to get a bijection $\USym { G \ltimes \tilde H } \weq \USymG \times \USymH$.
% Now use that to transport the multiplication operation of the group $\USym { G \ltimes \tilde H }$ to the set $\USymG \times \USymH$.
% Now \cref{lem:pathpairsectionmult} tells us the formula for that transported operation is given as follows.
% $$ (p',q') \cdot (p,q) = (p' \cdot p , ({q'} ^ p) \cdot q) $$
% In a traditional algebra course dealing with abstract groups, this formula is used as the definition of the multiplication operation
% on the set $\USymG \times \USymH$, but then one must prove that the operation satisfies the properties of \cref{def:abstractgroup}.
% The advantage of our approach is that the formula emerges from the underlying logic that governs how composition of paths works.

\section{The isomorphism theorems}
\label{sec:noether-theorems}

Cf.~\cref{sec:stuff-struct-prop}

Group homomorphisms provide examples of forgetting stuff and structure.
For example, the map from cyclically ordered sets with cardinality $n$
to the type of sets with cardinality $n$ forgets structure,
and represents an injective group homomorphism from the cyclic
group of order $n$ to the symmetric group $\Sigma_n$.

And the map from pairs of $n$-element sets to $n$-element sets
that projects onto the first factor clearly forgets stuff,
namely, the other component.
It represents a surjective group homomorphism.

More formally, fix two groups $G$ and $H$,
and consider a homomorphism $\varphi$ from $G$ to $H$,
considered as a pointed map $\B\varphi : \BG \to_\pt \BH$.
Then $\B\varphi$ factors as
\begin{align*}
  \BG
  = &\sum_{w:\BH}\sum_{z:\BG}(\B\varphi(z)=w)\\
  \to_\pt &\sum_{w:\BH}\;\Trunc[\Big]{\sum_{z:\BG}(\B\varphi(z)=w)}_0\\
  \to_\pt &\sum_{w:\BH}\;\Trunc[\Big]{\sum_{z:\BG}(\B\varphi(z)=w)}_{-1} = \BH.
\end{align*}
The pointed, connected type in the middle represents a group
that is called the \emph{image} of $\varphi$, $\Img(\varphi)$.


(FIXME: Quotient groups as automorphism groups, normal subgroups/normalizer, subgroup lattice)

\begin{lemma}
  \label{lem:aut-orbit}
  The automorphism group of the $G$-set $G/H$ is isomorphic to $\N_G(H)/H$.
\end{lemma}

\begin{theorem}[Fundamental Theorem of Homomorphisms]
  \label{thm:fund-thm-homs}
  For any homomorphism $f : \Hom(G,G')$
  the map {\color{blue} TODO} defines an isomorphism
  $G/\ker f \simeq \im f$.\footnote{TODO: Fix and move to Ch. 5}
\end{theorem}

% Where does this go?!
\section{More about automorphisms}
\label{sec:automorphisms}

% Written to record somewhere the results of a discussion with Bjorn
For every group $G$ (which for the purposes of the discussion
in this section we allow to be a higher group)
we have the automorphism group $\Aut(G)$.
This is of course the group of self-identifications $G = G$ in the type of groups, $\Group$.
If we represent $G$ by the pointed connected classifying type $\BG$,
then $\Aut(G)$ is the type of pointed self-equivalences of $\BG$.

We have a natural forgetful map from groups to the type of connected groupoids.
Define the type $\Bunch$ to be the type of all connected groupoid.
If $X:\Bunch$, then all the elements of $X$ are merely isomorphic,
that is, they all look alike,
so it makes sense to say that $X$ consists of a \emph{bunch} of alike objects.

For every group $G$ we have a corresponding bunch, $\BG_\div$,
\ie{} the collection of $G$-torsors,
and if we remember the basepoint $\shape_G : \BG_\div$,
then we recover the group $G$.
Thus, the type of groups equivalent to the type
$\sum_{X : \Bunch} X$
of pairs of a bunch together with a chosen element.
(This is essentially our definition of the type $\Group$.)

Sometimes we want to emphasize that we $\BG_\div$ is a bunch,
so we define $\bunch(G) \defeq \BG_\div : \Bunch$.

\begin{definition}[The center as an abelian group]
  \label{def:center}
  Let
  $$Z(G) \defeq \prod_{z : \BG}(z = z)$$ denote the type of fixed points of the adjoint action of $G$ on itself.
  This type is equivalent to the automorphism group of the identity on $\bunch(G)$,
  and hence the loop type of
  \[
    \B Z(G) \defeq \sum_{f : \BG \to \BG} \merely{f \sim \id}.
  \]
  This type is itself the loop type of the pointed, connected type
  \[
    \B^2Z(G) \defeq \sum_{X : \Bunch}\Trunc{\bunch(G) = X}_0,
  \]
  and we use this to give $Z(G)$ the structure of an \emph{abelian} group,
  called the \emph{center} of $G$.
\end{definition}
There is a canonical homomorphism from $Z(G)$ to $G$ given by the pointed map
from $\B Z(G)$ to $\BG$ that evaluates at the point $\shape_G$.
The fiber of the evaluation map $e : \B Z(G) \to_\pt \BG$ is
\begin{align*}
  \fiber_e(\shape_G)
  &\jdeq \sum_{f : \BG \to \BG} \merely{f \sim \id} \times (\mathop f \shape_G = \shape_G) \\
  &\equiv \sum_{f : \BG \to_\pt \BG} \merely{f \sim \id},
\end{align*}
and this type is the loop type of the pointed, connected type
\[
  \B\Inn(G) \defeq \sum_{H : \Group} \Trunc{\bunch(G) = \bunch(H)}_0,
\]
thus giving the homomorphism $Z(G)$ to $G$ a normal structure with
quotient group $\Inn(G)$, called the \emph{inner automorphism group}.

Note that there is a canonical homomorphism from $\Inn(G)$ to $\Aut(G)$
given by the pointed map $i : \B\Inn(G) \to \B\Aut(G)$ that forgets the component.
On loops, $i$ gives the inclusion into $\Aut(G)$ of the subtype of automorphisms of $G$
that become merely equal to the identity automorphism of $\bunch(G)$.
The fiber of $i$ is
\begin{align*}
  \fiber_i(\shape_G)
  &\jdeq \sum_{H : \Group} \Trunc{\bunch(G) = \bunch(H)}_0 \times (H = G) \\
  &\equiv \Trunc{\bunch(G) = \bunch(G)}_0.
\end{align*}
This is evidently the type of loops in the pointed, connected groupoid
\[
  \B\Out(G) \defeq \Trunc*{\sum_{X : \Bunch}\merely{\bunch(G) = X}}_1,
\]
thus giving the homomorphism $\Inn(G)$ to $\Aut(G)$ a normal structure with
quotient group $\Out(G)$, called the \emph{outer automorphism group}.
Note that $\Out(G)$ is always a $1$-group,
and that it is the decategorification of $\Aut(\bunch(G))$.

\begin{theorem}
  Let two groups $G$ and $H$ be given.
  There is a canonical action of $\Inn(H)$
  on the set of homomorphisms from $G$ to $H$, $\Trunc{\BG \to_\pt \BH}_0$.
  This gives rise to an equivalence
  \[
    \Trunc{\BG_\div \to \BH_\div}_0 \equiv \Trunc*{\left(\Trunc{\BG \to_\pt \BH}_0\right) _{h\Inn(H)}}_0
  \]
  between the set of maps from $\bunch(G)$ to $\bunch(H)$ and the set of
  components of the orbit type of this action.
\end{theorem}
\begin{proof}
  We give the action by defining a type family $X : \B\Inn(H) \to \UU$ as follows
  \[
    X\, \angled{K,\phi} \defeq \Trunc{\Hom(G,K)}_0 \jdeq \Trunc{\BG \to_\pt \BK}_0,
  \]
  for $\angled{K,\phi} : \B\Inn(H) \jdeq \sum_{K : \Group} \Trunc{\bunch(H) = \bunch(K)}_0$.
  Now we can calculate
  \begin{align*}
    \Trunc{X_{\Inn(H)}}_0
    &\jdeq \Trunc*{\sum_{K:\Group}\Trunc{\bunch(H)=\bunch(K)}_0\times\Trunc{\Hom(G,K)}}_0 \\
    &\equiv \Trunc*{\sum_{K:\Group}(\bunch(H)=\bunch(K))\times\Hom(G,K)}_0 \\
    &\equiv \Trunc*{\sum_{K:\Bunch}\sum_{k:K}(\bunch(H)=K)\times\sum_{f:\bunch(G)\to K)}\mathop f \pt = k}_0 \\
    &\equiv \Trunc*{\sum_{K:\Bunch} (\bunch(H)=K) \times(\bunch(G) \to K)}_0 \\
    &\equiv \Trunc*{\bunch(G)\to\bunch(H)}_0 \jdeq \Trunc*{\BG_\div \to \BH_\div}_0.\qedhere
  \end{align*}
\end{proof}

% \section{Orbit type as a groupoid completion(*)}
%deleted BID 211116
% \emph{This is a somewhat advanced topic that should occur much later, if at all.}

% \bigskip

% Suppose $G$ is a group acting on a groupoid $X$,
% given by a map $X : \BG \to_\pt \B\!\Aut(X_0)$,
% with $e_X : X(\pt) = X_0$.
% By induction on $e_X$ we may assume that $X_0\jdeq X(\pt)$
% and $e_X\jdeq\refl{}$.

% We have the orbit type $X_{hG} \jdeq \sum_{T:\BG}X(T)$.
% We think of this as identifying elements of $X_0$
% that are in the same orbit,
% in the sense that there are new identifications of $x$ and $y$
% for group elements $g$ with $g\cdot x = y$.

% In this section we study one way of making this intuition precise.

% Consider the pregroupoid $C_G(X)$ with object type $X_0$ and morphism sets
% \[
%   \hom(x,y) \defeq \sum_{g:G}(g\cdot x = y),
% \]
% where $g\cdot x \defeq g_*(x)$. The identity at $x$ is
% $(1,\id)$, while the composite of $(g,p):\hom(x,y)$ with
% $(h,q):\hom(y,z)$ is $(hg,r)$, where $r$ is built from $p$ and $q$ as
% follows:
% \[
%   hg \cdot x = h\cdot(g\cdot x) = h\cdot y = z.
% \]

% We have a functor of pregroupoids $F: C_G(X) \to X_{hG}$
% defined on objects by
% $F(x) := (\pt,x)$ and on morphisms $(g,p):\hom(x,y)$ by $F(g,p) :=
% (g,p)^=$.

% This functor is essentially surjective on objects (by connectivity of
% $\BG$) and fully faithful by the characterization of paths in
% $\sum$-types. Hence it induces an equivalence from the completion of
% $C_G(X)$ to $X_{hG}$.

% As a corollary, the orbit set $X/G \jdeq \Trunc{X_{hG}}_0$,
% is the set quotient of $X_0$ modulo the equivalence relation
% $x \sim y \defeq \exists g:G, g\cdot x = y$.

%%% Local Variables:
%%% mode: latex
%%% fill-column: 144
%%% TeX-master: "book"
%%% End: