\chapter{Symmetry}
\label{ch:symmetry}

\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}
\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 $\sh_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 $\USym G$ 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}(\USym H)$.
\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 $\USym H$
that arise as $r \mapsto p\inv q r$ for $p,q\in \USym H$.

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=\USym H)$ 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 $(\USym H,(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 identity 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(\sh_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 $(\sh_G,\sh_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,\sh_{\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 (\sh_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}(\sh_G)$ defined by
  $ u \mapsto ((\sh_G,u), \refl{\sh_G}) $ is an equivalence.   This establishes that the fiber $(\B p)^{-1}(\sh_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 \USym G \times \USym H$.
Now use that to transport the multiplication operation of the group $\USym { G \ltimes \tilde H }$ to the set $\USym G \times \USym H$.
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 $\USym G \times \USym H$, 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{Orbit-stabilizer theorem}
\label{sec:orbit-stabilizer-theorem}

Given an action $X : \BG \to \UU$ and a point $x : X(\pt)$, we define
the \emph{orbit} through $x$ as the subtype of $X(\pt)$ consisting of
all $y : X(\pt)$ that are merely equal to $x$ in the orbit type:
\[
  G\cdot x \defeq \mathcal O_x \defeq \sum_{y : X(\pt)} \merely{[x] = [y]}
\]
(Note the unfortunate terminology: an orbit is not an element in the
orbit type!) 
Note that this only depends on the image of $x$ in the set of orbits,
thus justifying the names. 

In this way, the type $X(\pt)$ splits as a disjoint union of orbits,
indexed by the set of orbits
\[
  X(\pt) \equiv \coprod_{z : X / G} \mathcal O_z. 
\]

The \emph{stabilizer group} $G_x$ of $x : X(\pt)$ is the automorphism group of $[x]$ in the orbit type. 
Different points in the same orbit have conjugate stabilizer groups. 

We say that the action is \emph{free} if all stabilizer groups are trivial. 

\begin{theorem}[Orbit-stabilizer theorem]
  \label{thm:orbitstab}
  Fix a $G$-type $X$ and a point $x : X(\pt)$.
  There is a canonical action $\tilde G : \BG_x \to \UU$,
  acting on $\tilde G(\pt)\equiv G$
  with orbit type $\tilde G\dblslash G_x \equiv \mathcal O_x$.
\end{theorem}
\begin{proof}
  Define $\tilde G(x,y,!)  \defeq (\pt = x)$.
\end{proof}

Now suppose that $G$ is a $1$-group acting on a set. 
We see that the orbit type is a set
(and is thus equivalent to the set of orbits)
if and only if
all stabilizer groups are trivial,
\ie if and only if the action is free. 

If $G$ is a $1$-group,
then so is each stabilizer-group,
and in this case (of a set-action),
the orbit-stabilizer theorem
tells us that

\begin{theorem}[Lagrange's Theorem]\footnote{insert that the action is free (referred to)}
\label{thm:lagrange}
  If $H \to G$ is a subgroup, then $H$ has a natural action on $G$,
  and all the orbits under this action are equivalent. 
\end{theorem}

% Interaction with cardinality: if G acts freely on S, then card(S/G) = card(S)/card(G)

\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*{\sum_{z:\BG}(\B\varphi(z)=w)}_0\\
  \to_\pt &\sum_{w:\BH}\Trunc*{\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}

\section{(the lemma that is not) Burnside's lemma}
\label{sec:burnsides-lemma}
\label{lem:burnsides-lemma}

\begin{lemma}
  \label{lem:burnside}
  Let $G$ be a finite group acting on a finite set $X$.
  Then the set of orbits is finite with cardinality
  \[
    \Card(X/G) = \frac1{\Card(G)}\sum_{g:\El G}\Card(X^g),
  \]
  where $X^g = \setof{x:X}{gx=x}$ is the set of elements
  that are fixed by $g$.
\end{lemma}
\begin{proof}
  Since $X$ and $G$ is finite, we can decide equality of their elements. 
  Hence each $X^g$ is a finite set, and since $G$ is finite,
  we can decide whether $x,y$ are in the same orbit by searching
  for a $g : \El G$ with $gx = y$.
  Hence the set of orbits is a finite set as well. 

  Consider now the set $R \defeq \sum_{g:\El G} X^g$,
  and the function $q : R \to X$
  defined by $q(g,x) \defeq x$.
  The map $q^{-1}(x) \to G_x$ that sends $(g,x)$ to $g$ is a bijection. 
  Thus, we get the equivalences
  \[
    R \jdeq \sum_{g:\El G} X^g \equiv \sum_{x:X} G_x
    \equiv \sum_{z:X/G} \sum_{x : \mathcal O_z} G_x,
  \]
  where the last step writes $X$ as a union of orbits. 
  Within each orbit $\mathcal O_z$,
  the stabilizer groups are conjugate,
  and thus have the same finite cardinality,
  which from the orbit-stabilizer theorem (\cref{thm:orbit-stabilizer}),
  is the cardinality of $G$ divided by the cardinality of $\mathcal O_z$.
  We conclude that $\Card(R) = \Card(X/G)\Card(G)$, as desired. 
\end{proof}

% 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 $\pt : \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 $\pt$.
The fiber of the evaluation map $e : \B Z(G) \to_\pt \BG$ is
\begin{align*}
  \fiber_e(\pt)
  &\jdeq \sum_{f : \BG \to \BG} \merely{f \sim \id} \times (\mathop f \pt = \pt) \\
  &\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(\pt)
  &\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*{\Trunc{\BG \to_\pt \BH}_0 \dblslash \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(*)}

\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\dblslash G \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 \dblslash G$
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\dblslash G$.

As a corollary, the orbit set $X/G \jdeq \Trunc{X \dblslash G}_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:
