absgroup.tex

\chapter{Groups, abstractly}
\label{ch:absgroup}

\section{Brief overview of the chapter}
Recall from \cref{sec:identity-type-as-abstract} the definition of an 
abstract group and how to obtain an abstract group from a concrete one. 
In this chapter we will 
implement an inverse construction, how to obtain a (concrete) group from
an abstract one, in \cref{sec:Gsetforabstract}. Likewise, in \cref{sec:homabsisconcr},
we show how to obtain a (concrete) homomorphism from an abstract one.
Thus we will have shown that, in principle,\footnote{%
Of course this is not a reason to stop here, but to continue
finding out which parts of group theory benefit from the concrete approach.
Just to mention a few we have seen already: 
the conceptual simplicity of homomorphisms being pointed maps,
actions being maps from the classifying type to $\Set$, 
and the generalizations to \inftygps indicated in \cref{ch:actions}.}
it doesn't matter whether
one develops group theory on the concrete or on the abstract level.

Before we implement the above constructions, 
we first introduce in \cref{sec:monoids} a simpler structure, 
called monoid, of which abstract groups are a special case.\footnote{%
One could advocate for the name `abstract monoid' here, were it not the
case that we have no concrete analogue for monoids in our setting.
The reason is the symmetry of the identity types.}
We then define in \cref{sec:abshom} the notion of homomorphism for
abstract groups.

After groups and homomorphism, it is natural to continue to group actions,
in \cref{sec:Gsetsabstrconcr}, and again relate the abstract to the concrete.

 In the optional~\cref{sec:heaps} we look at how general
identities types $a \eqto_A a'$ relate to groups.

\section{Monoids and abstract groups}
\label{sec:monoids}

  A monoid is a collection of data consisting only of \ref{struc:under-set}, 
  \ref{struc:unit}, and \ref{struc:mult-op} from the list in
  \cref{def:abstractgroup}.
  In other words, the existence of inverses is not assumed.
  For convenience we reproduce the shortened list here.

\begin{definition}\label{def:monoid}
  A \emph{monoid}\index{monoid} consists of the following data.
  \begin{enumerate}
  \item\label{struc:monoid-set} A set $S$, called the \emph{underlying set}.
  \item\label{struc:monoid-unit} An element $e:S$, called the \emph{unit} or the \emph{neutral element}.\index{neutral element}
  \item\label{struc:monoid-mult} A function $S\to S\to S$, called \emph{multiplication},
    taking two elements $g_1,g_2:S$ to their \emph{product}, denoted by $g_1\cdot g_2:S$.
    \par \noindent
    Moreover, the following equations should hold, for all $g,g_1,g_2,g_3 : S$.
    \begin{enumerate}[label=(\alph*),ref=\ref{struc:monoid-mult} (\alph*)]
    \item\label{monoid:unit-laws} $g\cdot e=g$ and $e\cdot g=g$ (the \emph{unit laws})
    \item\label{monoid:ass-law} $g_1\cdot(g_2\cdot g_3)=(g_1\cdot g_2)\cdot g_3$ 
         (the \emph{associativity law})
    \end{enumerate}
  \end{enumerate}
 The property that $S$ is a set, the
  unit laws, and the associativity law, are together known as the \emph{monoid laws}.
\end{definition}


  Building on the definition of a monoid, we may encode the type of abstract 
  groups as follows. We let $S$ denote the underlying set, $e : S$ denote the unit, 
  $\mu:S\to S\to S$ denote the multiplication operation 
  $g\mapsto (h \mapsto g\cdot h)$, and $\iota : S \to S$ denote 
  the inverse operation $g \mapsto g^{-1}$.  Using
  that notation, we introduce names for the relevant propositions.
  \begin{align*}
    \mathrm{UnitLaws}(S,e,\mu)   & \defequi
    \prod_{g:S} \bigl((\mu{}(g)(e) = g)\times(\mu{}(e)(g) = g) \bigr)\\
    \mathrm{AssocLaw}(S,\mu{})   & \defequi\prod_{g_1,g_2,g_3:S} 
    \bigl( \mu{}(g_1)(\mu{}(g_2)(g_3))=\mu{}(\mu{}(g_1)(g_2))(g_3) \bigr)\\
    \mathrm{MonoidLaws}(S,e,\mu) & \defequi \isset{(S)} 
    \times \mathrm{UnitLaws}(S,e,\mu) \times \mathrm{AssocLaw}(S,\mu{}) \\
    \mathrm{InverseLaw}(S,e,\mu,\iota) & \defequi 
    \prod_{g:S}\bigl( \mu(g)(\iota(g)) = e \bigr) \\
    \mathrm{GroupLaws}(S,e,\mu,\iota) & \defequi 
    \mathrm{MonoidLaws}(S,e,\mu) \times \mathrm{InverseLaw}(S,e,\mu,\iota)
  \end{align*}

\begin{definition}
  \label{def:type-abstrgp}
  Recall the definition of abstract group in \cref{def:abstractgroup}.
  \index{type!of abstract groups}
  \glossary(Groupabs){$\protect\typeabsgp$}{type of abstract groups}
  The type of abstract groups is
  \[
    \typeabsgp \defequi \sum_{S:\UU} \sum_{e:S}\sum_{\mu{}:S\to S\to S}
    \sum_{\iota\colon S\to S} \mathrm{GroupLaws}(S,e,\mu,\iota).\qedhere
  \]
\end{definition}

  Thus, following the convention introduced in \cref{rem:iterated-sums},
  an abstract group $\mathscr G$ will be a quintuple of the form
  $\mathscr G \jdeq (S,e,\mu,\iota,!)$.  For brevity, we will usually 
  omit the proof of the properties from the display, since it's unique,
  and write an abstract group as though it were a quadruple 
  $\mathscr G \jdeq (S,e,\mu,\iota)$.


\begin{remark}\label{rem:inverses-as-property}
  Instead of including the inverse operation as part
  \ref{monoid:inv-op} of the structure (including the property
  \ref{monoid:inv-law}), some authors assume the existence of inverses
  by positing the property \ref{monoid:inv-law} below.
  \begin{enumerate}[start=4]
    \item\label{monoid:inv-op} A function $(\blank)^{-1}:S\to S$, 
    the \emph{inverse operation}, satisfying:
    \begin{enumerate}[start=3,label=(\alph*),ref=\ref{monoid:inv-op} (\alph*),resume*]
    \item\label{monoid:inv-law} $g\cdot g^{-1} = e$ for all $g:S$ (the \emph{law of inverses}).
    \end{enumerate}
    \item\label{axiom:mere-inverse} For all $g:S$ there exists an element
    $h:S$ such that $e = g \cdot h$.
  \end{enumerate}

  We will now compare \ref{axiom:mere-inverse} to \ref{monoid:inv-op}.
  Property \ref{axiom:mere-inverse} contains the phrase ``there exists'', and thus its translation into type theory
  uses the quantifier $\exists$, as defined in \cref{sec:prop-trunc}.  Under this translation, property \ref{axiom:mere-inverse} does
  not immediately allow us to speak of ``the inverse of $g$''.
  However, the following lemma shows that we can define an inverse operation as in \ref{monoid:inv-op} from a witness of \ref{axiom:mere-inverse}
  -- its proof goes by using the unit laws \ref{monoid:unit-laws} and the
associativity law \ref{monoid:ass-law} to prove that inverses are unique.  
As a consequence, we can speak of ``\emph{the} inverse of $g$''.
\end{remark}

\begin{lemma}%
  \label{lem:group-inv-operation}%
  Given a set $S$ together with $e$ and $\cdot$ as in
  \cref{def:monoid} satisfying the unit laws, the associativity
  law, and property \ref{axiom:mere-inverse}, we have a unique ``inverse'' function
  $S \to S$ having property \ref{axiom:inv-law} of \cref{def:abstractgroup}.
\end{lemma}

\begin{proof}
  Consider the function $\mu: S \to (S \to S)$ defined as
  $g\mapsto (h \mapsto g\cdot h)$. Let $g:S$. We claim that the fiber
  $\inv{\mu(g)}(e)$ is contractible.  Contractibility is a proposition, 
  hence to
  prove it from \ref{axiom:mere-inverse}, one can as well assume the
  actual existence of $h$ such that $g\cdot h = e$. Then $(h,!)$ is an
  element of the fiber $\inv{\mu(g)}(e)$. We will now prove that it is
  a center of contraction. For any other element $(h',!)$, we want to
  prove $(h,!) = (h',!)$, which is equivalent to the equation $h=h'$. In
  order to prove the latter, we show that $h$ is also an inverse on
  the left of $g$, meaning that $h\cdot g=e$.  This equation is also a
  proposition, so we can assume from \ref{axiom:mere-inverse} that we have an
  element $k:S$ such that $h\cdot k = e$.  Multiplying that equation by
  $g$ on the left, one obtains
  \begin{displaymath}
    k = e \cdot k = (g\cdot h)\cdot k = g\cdot (h\cdot k) = g\cdot e = g,
  \end{displaymath}
  from which we see that $h\cdot g=e$.
  Now it follows that
  \begin{displaymath}
    h = h \cdot e = h \cdot (g\cdot h') = (h \cdot g) \cdot h' = e \cdot h' = h',
  \end{displaymath}
  as required. Hence $\inv{\mu(g)}(e)$ is contractible, and we may define $g^{-1}$ to
  be the center of the contraction, for any $g:S$.
  The function $g \mapsto \inv g$ satisfies the law of inverses 
  \ref{monoid:inv-law}, as required.\footnote{%
  Note that this proof also shows that  $\inv{(\inv g)} = g$ and hence
  $\inv g \cdot g = e$, for any $g:S$.}
  Since the inverse of each $g:S$ is unique, it follows by function
  extensionality that this `inverse' function is unique.
\end{proof}

\begin{remark}
  That the concept of an abstract group synthesizes the idea of symmetries
  will be justified in \cref{sec:Gsetforabstract} where we prove that
  the function $\abstr:\typegroup\to\typegroup^{\abstr}$ from 
  \cref{def:abstrG} is an equivalence.
\end{remark}

\begin{remark}\label{rem:abs-iso}
  If $\agp G\jdeq (S,e,\mu,\iota)$ and $\agp G'\jdeq(S',e',\mu',\iota')$
  are abstract groups, an element of the identity type
  $\agp G\eqto\agp G'$ consists of quite a lot of information,
  provided we interpret it by repeated application of \cref{lem:isEq-pair=}.
  First and foremost, we need an identification $p:S\eqto S'$ of sets, but
  from there on the information is a proof of a conjunction of propositions.\footnote{%
    \label{ft:no-abs-inftygp}
    Even though we are able to give a concise definition of \inftygps 
    in \cref{sec:inftygps}, we don't know how to define
    the type of ``abstract \inftygps'' in a way similar
    to~\cref{def:abstractgroup}:
    such a definition would require infinitely many 
    levels of operations producing
    identifications of instances of operations of lower levels.
    And an identification would similarly require infinitely
    many operations identifying the operations at all levels.
    See also \cref{rem:ee=e_coherence}.}
  An analysis shows that this conjunction can be shortened to the equations $e'=p(e)$ and
  $\mu'(p(s),p(t))=p(\mu(s,t))$.  A convenient way of obtaining an 
  identity $p$ that preserves these equations is to apply univalence to an
  equivalence $f: S \equivto S'$ that preserves them.
  We call such a function $f$ an \emph{isomorphism of abstract groups}.%
  \index{isomorphism!of abstract groups}
\end{remark}

\begin{xca}
  Perform the abovementioned analysis.
\end{xca}

\begin{xca}
  \label{xca:op-abs-group}
  Let $\agp G \jdeq (S,e,\mu,\iota)$ be an abstract group.
  Define another structure $\agp G\op \defeq (S,e,\mu\op,\iota)$,
  where $\mu\op : S \to S \to S$ sends $a,b:S$ to $\mu(b,a)$,
  \ie $\mu\op$ swaps the order of the arguments as compared to $\mu$.

  Show that $\iota : S \to S$ defines an isomorphism 
  $\agp G \equivto \agp G\op$.\footnote{%
  Hint: in down-to-earth terms this boils down to the equations
  $\inv e = e$ and $(a\cdot b)^{-1} = b^{-1}\cdot a^{-1}$.}
\end{xca}

\begin{xca}
  \label{xca:conj}
  Let $\agp G\jdeq(S,e,\mu,\iota)$ be an abstract group and let $g:S$.  
  For any $s:S$, let $\conj^g(s)\defequi g\cdot s\cdot g^{-1}$. 
  Show that the resulting function $\conj^g:S\to S$ preserves the group 
  structure (\eg $g\cdot(s\cdot s')\cdot g^{-1}=(g\cdot s\cdot g^{-1} )\cdot(g\cdot s\cdot g^{-1})$) and is an equivalence.  The resulting identification $\conj^g:\agp G\eqto\agp G$ is called \emph{conjugation} by $g$.\index{conjugation}
\end{xca}

\begin{remark}\label{rem:ee=e_coherence}
  Without the requirement that the underlying type of an abstract group or monoid 
  is a set, life would be more complicated.  For instance, for the
  case when $g$ is $e$, the unit laws \ref{monoid:unit-laws} of \cref{def:monoid}
  would provide \emph{two} (potentially different)
  identifications $e\cdot e \eqto e$, and we would have to separately 
  assume that they agree.  This problem vanishes in the setup we adopted for
  \inftygps in \cref{sec:inftygps}.
\end{remark}

\begin{xca}\label{xca:left-inv-involution}
  Given an element $g$ in an abstract group,
  prove that $e=\inv g\cdot g$ and $g=(g^{-1})^{-1}$. 
  (Hint: study the proof of \cref{lem:group-inv-operation}.)
\end{xca}

\begin{xca}\label{xca:typemonoidisgroupoid}
  Prove that the types of monoids and abstract groups are groupoids.
\end{xca}

\begin{xca}
  \label{xca:cheapgroup}
  There is a leaner way of characterizing what an abstract group is:
  define a \emph{sheargroup} to be a set $S$ together with an element $e:S$,
  a function $\blank * \blank: S\to S\to S$, sending $a,b:S$ to $a*b:S$,
  and the following propositions,
  where we use the shorthand $\bar a\defequi a*e$:
  \begin{enumerate}
  \item $e*a=a$,
  \item $a*a=e$, and
  \item $c*(b*a)=\casoverline{(c*\bar b)}*a$,
  \end{enumerate}
  for all $a,b,c:S$.
  Construct an equivalence from the type of abstract groups to the type of sheargroups.\footnote{%
      Hint: setting $a\cdot b\defequi \bar b*a$ gives you an abstract group from a sheargroup and conversely, letting $a*b=b\cdot a^{-1}$ takes you back.  On your way you may need at some point to show that $\casoverline{\bar a}=a$: setting $c=\bar a$ and $b=a$ in the third formula will do the trick (after you have established that $\bar e=e$).  This exercise may be good to look back to in the many instances where the inverse inserted when ``multiplying from the right by $a$'' is forced by transport considerations.}
\end{xca}
\begin{xca}
  Another and even leaner way to define abstract groups, highlighting how we can do away with both the inverse and the unit: a \emph{Furstenberg group}\footnote{%
    Named after Hillel Furstenberg who at the age of 20 published a paper doing this exercise.\footnotemark{}}\footcitetext{Furstenberg}
  is a nonempty set $S$ together with a function
  $\blank\circ\blank : S \to S \to S$, sending $a,b:S$ to $a\circ b:S$,
  with the property that
  \begin{enumerate}
  \item for all $a,b,c:S$ we have that $(a\circ c)\circ(b\circ c)=a\circ b$, and
  \item for all $a,c:S$ there is a $b:S$ such that $a\circ b=c$.
  \end{enumerate}
  Construct an equivalence from the type of Furstenberg groups to the type of
  abstract groups.\footnote{%
    Hint: show that the function $a\mapsto a\circ a$ is constant, with value, say, $e$.  Then show that $S$ together with the ``unit'' $e$, ``multiplication'' $a\cdot b\defequi a\circ(e\circ b)$ and ``inverse'' $b^{-1}\defequi e\circ b$ is an abstract group.}
\end{xca}

\section{Abstract homomorphisms}\label{sec:abshom}

In this section we define the notion of homomorphism for
abstract groups, which we touched upon just above
\cref{exa:conj-concrete}. We start by an exercise
that simplifies the requirements for abstract group homomorphisms.

\begin{xca}\label{{xca:onlymult-hom}}
  Let $\agp G\defequi(S,e_{\agp G},\cdot_{\agp G},\iota_{\agp G})$
  and $\agp H\defequi(T,e_{\agp H},\cdot_{\agp H},\iota_{\agp H})$
  be abstract groups, and $f:S\to T$ a function satisfying
  $f(s\cdot_{\agp G}s')=_Tf(s)\cdot_{\agp H}f(s')$ for all $s,s':S$.
  Show that $f(e_{\agp G}) = e_{\agp H}$ and 
  $f(\iota_{\agp G}(s)) = \iota_{\agp H}(f(s))$ for all $s:S$.
\end{xca}

Thus we see that, due to the properties of the abstract groups,
if $f$ preserves multiplication, then $f$ also preserves unit and inverses.%
\footnote{\label{ft:monoid-hom}For monoids this is not true:
  Let $M$ be the monoid with two elements, $1$ and $\infty$,
  with a multiplication such that $1$ is the unit and
  $\infty*\infty=\infty$. Now consider $h: M\to M$
  defined by $h(m)=\infty$ for all $m:M$. Then $h$ preserves
  multiplication, but not the unit. Note that $M$ cannot
  be extended to an abstract group, since giving $\infty$
  an inverse would make it equal to $1$.}
  
\begin{definition}\label{def:abstrisfunctor}
  Let $\agp G\defequi(S,e_{\agp G},\cdot_{\agp G},\iota_{\agp G})$
  and $\agp H\defequi(T,e_{\agp H},\cdot_{\agp H},\iota_{\agp H})$
  be two abstract groups,\footnote{%
    Recall from~\cref{def:abstractgroup} that the components comprise
    the underlying set, the unit element, the multiplication,
    and the inverse operation. We also need the laws to hold, 
    but this notation elides the corresponding witnesses.

    In the display, 
    $f(s\cdot_{\agp G}s')=_Tf(s)\cdot_{\agp H}f(s')$ is a proposition; 
    hence a homomorphism of abstract groups is uniquely determined
    by its underlying function of sets, and unless there is danger of
    confusion we write $f$ instead of $(f,!)$.}
  then the set of homomorphisms from $\agp G$ to $\agp H$ is
  \[
    \absHom(\agp G,\agp H)
    \defequi\sum_{f:S\to T}
    \prod_{s,s':S}\bigl(f(s\cdot_{\agp G}s')=_Tf(s)\cdot_{\agp H}f(s')\bigr).
  \]
  \index{type!of abstract homomorphisms}\index{homomorphism!of abstract group}
  \glossary(){$\protect\absHom$}{type of abstract homomorphisms}
  For groups $G$ and $H$, the function
  \[
    \abstr:\Hom(G,H)\to\absHom(\abstr(G),\abstr(H))
  \]
  is defined as the function $f\mapsto \abstr(f)\defequi(\USymf,!)$
  made explicit in \cref{def:USym-hom} and satisfying the
  properties by~\cref{lem:grouphomomaxioms}.
\end{definition}

\begin{remark}\label{rem:monoid-hom}
  With our definition it is immediate that a homomorphism of abstract
  groups also defines a homomorphism of the underlying monoids,
  preserving multiplication and thereby unit. However,
  for monoids as defined in~\cref{def:monoid}, it is possible to preserve
  multiplication but not the unit, as shown in \cref{ft:monoid-hom}.
  Hence, for monoids we define the set of homomorphisms
  from $M \jdeq (S,e_M,\cdot_M)$ to $N \jdeq(T,e_N,\cdot_N)$ by
  \[
    \sum_{f:S\to T}\Bigl(\bigl(f(e_M) =_T e_N\bigr)\times
    \prod_{s,s':S}\bigl(f(s\cdot_M s')=_T f(s)\cdot_N f(s')\bigr)\Bigr).%
    \qedhere
  \]
\end{remark}

\begin{xca}
Prove that composition of the functions on the underlying sets gives a composition of homomorphisms of abstract groups.

  Prove that for $f_0:\Hom(G_0,G_1)$ and $f_1:\Hom(G_1,G_2)$ we have
  $$\abstr(f_1f_0)=\abstr(f_1)\abstr(f_0)$$ and that 
  $\abstr(\id_G)=\id_{\abstr(G)}$.
\end{xca}

\begin{example}
  \label{ex:conjhom}
  Let $\agp G=(S,e,\mu,\iota)$ be an abstract group and let $g:S$. 
  In \cref{xca:conj} we defined $\conj^g:S\to S$ by setting 
  $\conj^g(s)\defequi g\cdot s\cdot g^{-1}$ for all $s:S$,
  and asked you to show that it ``preserves the group structure'',
  \ie classifies a homomorphism
  \[
    \cong^g:\absHom(\agp G,\agp G)
  \]
  called \emph{conjugation} by $g$\index{conjugation}.
  Actually, we asked for more: namely that conjugation by $g$ is 
  an isomorphism, and hence determines an identification
  (for which we used the same symbol) $\conj^g:\agp G\eqto\agp G$.

  If $\agp H$ is some other abstract group, transport along $\conj^g$
  gives an identification
  $\conj^g_*:\Hom(\agp H,\agp G) \eqto \Hom(\agp H,\agp G)$
  which should be viewed as ``postcomposing with conjugation''.
  Similar considerations go for elements in $\agp H$,
  giving rise to ``precomposition with conjugation $\cong^h$''.
\end{example}

\section{Groups: from concrete to abstract and back}
\label{sec:Gsetforabstract}

We use \cref{lem:BGbytorsor} as our inspiration for trying to construct 
a group from an abstract group.
That is, in total analogy, we define the torsors for an abstract group,
and it will then be relatively simple to show that the constructions of
\begin{enumerate}
\item forming the abstract group of a group and
\item taking the group classified by the torsors of an abstract group
\end{enumerate}
 are inverse to each other.
\marginnote{%
Recall \cref{ft:no-abs-inftygp}, explaining why we do not consider an
``abstract'' counterpart of the concept of \inftygp.
Consequently, all we do in this section is set-based.
}

Let $G$ be a group and $X:\BG\to\Set$ a $G$-set. Using the
underlying set $X(\sh_G)$, we can restrict the
codomain of $X$ to $\Set_{(X(\sh_G))}$, the classifying type of 
$\SG_{X(\sh_G)}$. Then we can view $X$ as the classifying function of 
a group homomorphism from $G$ to $\SG_{X(\sh_G)}$.
We already know the abstract versions of all three ingredients,
the two groups and the homomorphism. Thus, the abstract version
of $X$ can be expected to consist of the set $X(\sh_G)$ and 
$\abstr(X)$, the abstract homomorphism from $\abstr(G)$ 
to $\abstr(\SG_{X(\sh_G)})$.

A case in point is the principal $G$-torsor $\princ G \jdeq
(z\mapsto (\sh_G\eqto z))$. Its underlying set is $\USymG$.
The abstract version of the corresponding homomorphism,
defined by transport, is the function $\USymG\to(\USymG\eqto\USymG)$
mapping $g$ to $(g\cdot\blank)$, \ie postcomposition with $g$.%
\footnote{\label{ft:choicePshG}A (free) choice has been made to define 
$\princ G$ using $(\sh_G\eqto z)$ and not $(z\eqto\sh_G)$. In the latter
case its abstract version would map $g$ to $(\blank\cdot\inv g)$,
precomposition with the inverse of $g$. See also \cref{xca:absprtorsor}.}
A small generalization now leads to the following definition.

\begin{definition}
\label{def:abstrGtorsors}
Given an abstract group ${\agp G}\jdeq(S,e,\mu,\iota)$, a \emph{$\agp G$-set}%
\glossary(GSet){\protect{$\absGSet$}}{type of $\agp G$-sets}
\index{GSet@$\agp G$-set (of abstract group)}
is a set $S$ together with a homomorphism
$\agp G\to\abstr(\Sigma_S)$
from $\agp G$ to the abstract permutation group of $S$.
Then the type of $\agp G$-sets is defined as 
$$\absGSet\defequi \sum_{S:\Set}\absHom({\agp G},\abstr(\Sigma_{S})).$$

The \emph{principal ${\agp G}$-torsor} $\absprtor$ is the 
${\agp G}$-set consisting of the underlying set $S$ together with 
the homomorphism ${\agp G}\to\abstr(\Sigma_{S})$ with underlying 
function $S\to (S\eqto S)$ given by sending $g:S$ to $(s\mapsto \mu(g,s))$.

The type of \emph{${\agp G}$-torsors} is
\[
\absGTor\defequi\sum_{\absGSetvar:\absGSet}
  \Trunc{\absprtor \eqto \absGSetvar}.\qedhere
\]
\end{definition}

\begin{xca}\label{xca:absprtorsor}
In the setting of the above definition,
give an identification of $(S,(s\mapsto \mu(g,s)))$ with
$(S,(s\mapsto \mu(s,\iota(g))))$
in the type $\absGSet$.\footnote{\MB{Mention co-group?}}
\end{xca}

\begin{example}
  Given a group $G$, recall from \cref{lem:idtypesgiveabstractgroups}
  that the abstract group is 
  $\abstr(G)\jdeq(\USymG,e_G,\cdot,\inv{(\blank)})$ 
  with $\USymG\jdeq(\sh_G\eqto\sh_G)$ and $e_G\jdeq\refl{\sh_G}$,
  and $\cdot$ and $\inv{(\blank)})$ as usual for paths.
  Unravelling the definition, and \cref{def:abstrisfunctor},
  we see that an $\abstr(G)$-set consists of
  \begin{enumerate}
  \item a set $S$, and
  \item a function $f:\USymG\to (S\eqto S)$ such that
  \item for all $p,q:\USymG$ we have that $f(p\, q)=f(p)\,f(q)$.\qedhere
  \end{enumerate}
\end{example}

To help reading the coming proofs we introduce some notation that is
redundant, but may aid the memory in cluttered situations.
Let $x,y,z$ be elements in some type, then define:%
\footnote{We recognize $\preinv$ from \cref{lem:pathsptransportiseq}
as the induced map of identity types $\pathsp{\blank}\colon (y\eqto x)
\to(\pathsp y \eqto \pathsp x)$, followed by evaluation at $z$.
Post-composition $\post$ is transport in the family $\pathsp x$,
while $\preinv$ is precomposition by the inverse of its argument.
We will sometimes write $\preinv_z$ to stress the variable $z$
in the type of $\preinv$, and likewise write $\post_x$.}
\begin{align*}
%  \pre:(x\eqto y)\to ((y\eqto z)\eqto (x\eqto z)),\qquad&\pre(q)(p)\defequi pq\\
  \preinv:(y\eqto x)\to ((y\eqto z)\eqto (x\eqto z)),\quad&\preinv(q)(p)\defequi\pathsp qp\defequi pq^{-1}\\
  \post:(y\eqto z)\to ((x\eqto y)\eqto (x\eqto z)),\quad&\post(p)(q)\defequi\post_pq\defequi pq
  %\adjoint:(x\eqto y)\to((x\eqto x)\eqto (y\eqto y)),\qquad&\adjoint(q)(p)\defequi\adjoint_qp\defequi qpq^{-1}
\end{align*}

\begin{example}\label{ex:qG}
  Given a group $G$ and $x:\BG$, the principal $G$-torsor
  \emph{evaluated at $x$}, \ie the set $\princ G(x)\jdeq (\sh_G\eqto x)$,
  has a natural structure of an $\abstr(G)$-set by means of
  $$\preinv_x:\USymG\to ((\sh_G\eqto x)\eqto (\sh_G\eqto x)).$$
  Indeed, $\preinv_x$ is an abstract homomorphism since,
  for all $p,q:\USymG$, we have that 
  $\preinv_x(p\,q)=\preinv_x(p)\preinv_x(q)$.% 
  \footnote{For any $r\colon \sh_G\eqto x$ we have that
  $\preinv_x(p\, q)(r)=r\,(p\,q)^{-1}=r\,q^{-1} p^{-1}=
  \preinv_x(p)(\preinv_x(q)(r))$.
  Without the inverse, this would have gone badly wrong.
  Moreover, referring to \cref{xca:absprtorsor},
  $\preinv$ is here more natural than $\post$:
  $\USymG$ consists of the symmetries of $\sh_G$, and the $x$ is fixed.}

  Furthermore, for any $x:\BG$, the $\abstr(G)$-set 
  $(\sh_G\eqto x,\preinv,!)$ is an $\abstr(G)$-torsor.
  Since this is a proposition and $\BG$ is connected, it suffices
  to verify this for $x\jdeq\sh_G$, for which it follows from
  \MB{\cref{xca:absprtorsor}}.
\end{example}

\begin{definition}
  If ${\agp G}$ is an abstract group, then the (concrete)
  \emph{group $\concr({\agp G})$ associated with ${\agp G}$} is the group
  classified by the pointed connected groupoid 
  $(\absGTor,\absprtor)$.
\end{definition}

We give the construction of \cref{ex:qG} \MB{???} a short 
name since it will occur in important places.
\begin{definition}
  Let $G$ be a group.
  The group homomorphism
  $$q_G:\Hom(G,\concr(\abstr(G)))$$
  is classified by the following function, which is pointed by
  \MB{\cref{xca:absprtorsor}}:
\[
  \Bq_G:\BG\ptdto (\absGTor[\abstr(G)],\absprtor[\abstr(G)]),\quad q_G(z)
  \defeq(\princ G(z),\preinv_z,!).\qedhere
\]
\end{definition}


{\large \MB{cursor}}

\begin{lemma}
  \label{lem:Groupsareidentitytypes}
For all groups $G$, the pointed function $q_G:G\ptdto\concr(\abstr(G))$
is a  equivalence.
\end{lemma}
\begin{proof}
  To prove that $\Bq_G$ is an equivalence it is, by \cref{cor:fib-vs-path}\ref{conn-fib-vs-path}, enough to show that if $x,y:\BG$ then the induced map
$$\Bq_G:(x\eqto_{\BG}y)\to (\Bq_G(x)\eqto \Bq_G(y))
$$
is an equivalence.
  Now, $\Bq_G(x)\eqto \Bq_G(y)$ can be unfolded to
$$
((\sh_G\eqto x),\preinv_x)\eqto_{\absGSet[\abstr(G)]}((\sh_G\eqto y),\preinv_y)$$
which, by \cref{def:pathover-trp} and \cref{lem:isEq-pair=}, is equivalent to
\[
\sum_{f:(\sh_G\eqto x)\equivto (\sh_G\eqto y)}
\prod_{g:\USymG} f\circ(\preinv_x(g))=(\preinv_y(g))\circ f.
\]
Under these identities, and using function extensionality,
$\Bq_G$ is given by (with the type of $f$ as above)
\[
\post_{\sh_G}:(x\eqto y)\to \sum_{f}
\prod_{g:\USymG}\,\prod_{p:\sh_G\eqto x}\bigl(f(p\inv g)= f(p)\inv g\bigr).
\]
Given a function $f$ such that
$\prod_{g:\USymG}\,\prod_{p:\sh_G\eqto x}\bigl(f(pg)= f(p)g\bigr)$,%
\footnote{No need to invert $g$ here.}
the preimage $\post_{\sh_G}^{-1}(f)$ unfolds to
$\sum_{r:x\eqto y}(f=\post_{\sh_G}(r))$. For proving that $\post_{\sh_G}$,
and hence $\Bq_G$, is an equivalence, we have to show that the
latter preimage is contractible. This goal is a proposition
and $\BG$ is connected, so we may assume that we have a 
path $p_0:\sh_G\eqto x$. Then any $r,s:x\eqto y$ such that
$\post_{\sh_G}(r)= f=\post_{\sh_G}(s)$ satisfy $r\,p_0=f(p_0)=s\,p_0$,
so that $r=s$. Thus the preimage is a proposition. It remains
to find an $r$ such that $f=\post_{\sh_G}(r)$. 
We take $r=f(p_0)\inv{p_0}$ and verify, using
the property of $f$, that for any $p:\sh_G\eqto x$
\[
f(p) = f(p_0(\inv{p_0}p)) = f(p_0)(\inv{p_0} p) = (f(p_0) \inv{p_0}) p
= \post_{\sh_G}(r)(p).\qedhere
\]
\end{proof}

\begin{example}
  \label{ex:abstrconcrG}
  Let ${\agp G}=(S,e,\mu,\iota)$ be an abstract group.
Then the underlying set of $\abstr(\concr({\agp G}))$ is 
$\absprtor \eqto_{\absGTor}\absprtor$.
Unraveling the definitions we see that this set is equivalent to%
\footnote{\MB{NB notation not abstract.}}
$$\sum_{p:S\eqto S}\prod_{q,s:S}(p(s\,q^{-1})=p(s)\,q^{-1}).
$$
Setting $s\defequi e$ and renaming $t\defequi q^{-1}$ in the last equation, we see that $p(t)=p(e)t$; that is $p$ is simply multiplication with an element $p(e):S$.  in other words, the function
$$r_{\agp G}:S\to  \sum_{p:S\eqto S}\prod_{q,s:S}(p(s\,q^{-1})=p(s)\,q^{-1}),\qquad r_{\agp G}(u)\defequi(u\cdot\,,!)
$$
is an equivalence of sets, which we by univalence is converted into an identity.
The abstract group structure of $\abstr(\concr({\agp G}))$ is given by it being the symmetries of $\absprtor$; translated to $\sum_{p:S\eqto S}\prod_{q,s:S}(p(s\,q^{-1})=p(s)\,q^{-1})$ this corresponds via the first projection to the symmetries of $S$.
This means that we need to know that if $u,v:S$ and consider the two symmetries $u\cdot,v\cdot:S\eqto S$, then their composite (the operation on the symmetry on $S$) is equal to $(u\cdot v)\cdot:S\eqto S$ (the abstract group operation), but this is true by associativity ($u\cdot(v\cdot s)=(u\cdot v)\cdot s$).  That $r_{\agp G}$ also sends $e:S$ to $\refl S$ is clear.
Hence our identity $r_{\agp G}$ underlies an identity of abstract groups
$$r_{\agp G}:{\agp G}\eqto_{\typegroup^{\abstr}}\abstr(\concr({\agp G})).$$
\end{example}

This shows that every abstract group encodes the symmetries of something essentially unique.  Summing up the information we get
\begin{theorem}
  \label{thm:Groupsareidentitytypes}
  Let ${\agp G}$ be an abstract group. Then
$${\abstr}:\typegroup\to\typegroup^{\abstr}$$ is an equivalence.
\end{theorem}

\section{Homomorphisms}
\label{sec:homabsisconcr}

Now that we know how to identify the type of groups with the type 
of abstract groups, it is natural to ask if the notion of group 
homomorphisms also coincide.

They do, and we provide two independent and somewhat different arguments.
Translating from group homomorphisms to abstract group homomorphisms is easy:
if $G$ and $H$ are groups, then we defined
$$\abstr:\Hom(G,H)\to\absHom(\abstr(G),\abstr(H))$$
in \cref{def:USym-hom} and \cref{def:abstrisfunctor} as the function
which takes a homomorphism, classified by a pointed map $f:\BG\ptdto\BH$,
to the induced map of identity types
$$\USymf \jdeq \loops\Bf:\USymG\to\USymH$$
together with the proof that this is an abstract group 
homomorphism from $\abstr(G)$ to $\abstr(H)$.

Going back is somewhat more involved, and it is here we consider
two approaches. The first is a compact argument showing directly how to
reconstruct a pointed map $\Bf:\BG\ptdto\BH$ from an abstract group
homomorphism from $\abstr(G)$ to $\abstr(H)$. The second translates 
back and forth via our equivalence between abstract and concrete groups.

The statement we are after is:
\begin{lemma}
  \label{lem:homomabstrconcr}
  If $G$ and $H$ are groups, then
$$\abstr:\Hom(G,H)\to\absHom(\abstr(G),\abstr(H))$$
is an equivalence.
\end{lemma}
and the next two subsections offer two proofs.



\sususe{``Delooping'' a group homomorphism}
\label{sec:delooping} %after Coquand, after Deligne
We now explore the first approach.
It might be helpful to review \cref{lem:S1-delooping}
for a simple example of delooping in the special case of the circle.
Here we elaborate the general case.

\begin{proof}
  Suppose we are given an abstract group homomorphism
$$f:\absHom(\abstr(G),\abstr(H))$$
and we explain how to build a map $\Bg:\BG \rightarrow \BH$ with
a path $p:\sh_H \eqto \Bg(\sh_G)$ such that $p f(\omega) = \Bg(\omega) p$
for all $\omega:\sh_G \eqto \sh_G$ (so that $g:\Hom(G,H)$ is a ``delooping'' of $f$, 
that is, $f=\abstr(g)$).%
\footnote{We will thus have displayed a map
$\mathrm{deloop}:\absHom(\abstr(G),\abstr(H))\to\Hom(G,H)$ with 
$({\abstr}\circ\mathrm{deloop})=\id$. We leave it to the reader 
to prove that $\mathrm{deloop}\circ{\abstr}=\id$. }

To get an idea of our strategy, let us assume the problem solved. The map $\Bg:\BG\rightarrow \BH$
will then send any path $\alpha:\sh_G \eqto x$ to a path $\Bg(\alpha):\Bg(\sh_G) \eqto \Bg(x)$
and so we get a family of paths $p(\alpha) \defequi \Bg(\alpha) p$ in ${\sh_H} \eqto \Bg(x)$ such that
$$p(\alpha\omega) = \Bg(\alpha)\Bg(\omega)p
  = \Bg(\alpha)pf(\omega) = p(\alpha)f(\omega)$$
for all $\omega:\sh_G \eqto \sh_G$ and $\alpha : \sh_G \eqto x$.

This suggests to introduce the following family
$$
C(x)~:=~ \sum_{y:\BH}\sum_{p:(\sh_G \eqto x)\rightarrow (\sh_H \eqto y)}~~~\prod_{\omega:\sh_G \eqto {\sh_G}}\prod_{\alpha:\sh_G \eqto x}~
 p(\alpha\omega) = p(\alpha)f(\omega)
$$
 An element of $C(x)$ has three components, the last component being
 a proposition since $\BH$ is a groupoid.

 The type $C({\sh_G})$ has a simpler description. An element of $C({\sh_G})$ is
 a pair $y,p$ such that $p(\alpha\omega) = p(\alpha)f(\omega)$ for
 any $\alpha$ and $\omega$ in $\sh_G \eqto {\sh_G}$.
 Since $f$ is an abstract group homomorphism, this condition
 can be simplified to $p(\omega) = p(\refl{\sh_G})f(\omega)$, and the map $p$
 is completely determined by $p(\refl{\sh_G})$.
 Thus $C({\sh_G})$ is equal to $\sum_{y:\BH}\sh_H \eqto y$ and is contractible.


 It follows that we have\footnote{\MB{Why not skip next 3 lines?}}
 $$
 \prod_{x:\BG}~ (\sh_G \eqto x)\rightarrow\iscontr~ C(x)
 $$
and so, since $\iscontr~C(x)$ is a proposition
 $$
 \prod_{x:\BG}~ \Trunc{\sh_G \eqto x}\rightarrow\iscontr~ C(x)
 $$
 Since $\BG$ is connected, we have
 $\prod_{x:\BG}\iscontr~ C(x)$
 and so, in particular, we have an element of $\prod_{x:\BG}C(x)$.

 By projecting out the centers we get a map $\Bg:\BG\rightarrow \BH$
 together with a map $p:({\sh_G}\eqto x)\rightarrow ({\sh_H} \eqto \Bg(x))$ 
 such that $p (\alpha\omega) = p(\alpha) f(\omega)$
 for all $\alpha$ in $\sh_G \eqto x$ and $\omega$ in $\sh_G \eqto {\sh_G}$.
We have, for $\alpha:\sh_G \eqto x$
$$\prod_{x':\BG}\prod_{\lambda:x\eqto x'}~p(\lambda\alpha) = \Bg(\lambda)p(\alpha)$$
since this holds for $\lambda = \refl x$.
In particular, $p(\omega) = \Bg(\omega)p(\refl{\sh_G})$.

We also have $p(\omega) = p(\refl{\sh_G})f(\omega)$, hence
$p(\refl{\sh_G})\Bg(\alpha) =  f(\alpha)p(\refl{\sh_G})$
for all $\alpha:\sh_G\eqto \sh_G$ and we have found a delooping of $f$.
\end{proof}


\sususe{The concrete vs. abstract homomorphisms via torsors.}
\label{sec:absconctorsor}

The second approach to \cref{lem:homomabstrconcr} is as follows:


\begin{proof}
  The equivalence of $\pathsp{}^G:\BG\we(\typetorsor_G,\princ G)$ of \cref{lem:BGbytorsor} gives an equivalence
$$\pathsp{}:\Hom(G,H)\we((\typetorsor_G,\princ G)\ptdto(\typetorsor_H,\princ H))
$$
Consider the map
$$A:((\typetorsor_G,\princ G))\ptdto(\typetorsor_H,\princ H)\to \absHom(\abstr(G),\abstr(H))$$
given by letting $A(f,p)$ be the composite
$$\xymatrix{\USymG\ar@{=}[d]^{\pathsp{}^G}_\downarrow&&&
  \USymH\ar@{=}[d]^{\pathsp{}^H}_\downarrow\\
  (\princ G=\princ G)\ar[r]^-f&
  (f\princ G=f\princ G)\ar@{=}[rr]^-{q\mapsto p^{-1}qp}_\to&&
  (\princ H=\princ H)
}$$
(together with the proof that this is an abstract group homomorphism).  We
are done if we show that $A$ is an equivalence.
\marginnote{The reason to complicate $\abstr$ this way is that it gets easier to write out the inverse function.}

If $(\phi,!):\absHom(\abstr(G),\abstr(H))$ and $X:\BG\to\Set$ is a $G$-torsor, recall the induced $H$-torsor $\phi_*X$ from \cref{rem:inducedGsetfromabstracthomomorphisms} and the identity $\eta_\phi:\phi_*\princ G=\princ H$.
Let
$$B: \absHom(\abstr(G),\abstr(H))\to ((\typetorsor_G,\princ G)\ptdto(\typetorsor_H,\princ H)$$
be given by $B(\phi,!)=(\phi_*X,\eta_\phi)$

We show that $A$ and $B$ are inverse equivalences.  Given an abstract group homomorphism $(\phi,!):\absHom(\abstr(G),\abstr(H))$, then $AB(\phi,!)$ has as underlying set map
$$\xymatrix{\USymG\ar@{=}[d]^{\pathsp{}^G}_\downarrow&&&
  \USymH\ar@{=}[d]^{\pathsp{}^H}_\downarrow\\
  (\princ G=\princ G)\ar[r]^-{\phi_*}&
  (\phi_*\princ G=\phi_*\princ G)\ar@{=}[rr]^-{q\mapsto \eta_\phi^{-1}q\eta_\phi}_\to&&
  (\princ H=\princ H),
}$$
and if we start with a $g:\USymG$, then $\pathsp{}^G$ sends it to $\pathsp g^G\oldequiv\preinv (g)$.  Furthermore, $\phi_*\preinv (g)$ is $[\id,\preinv (g)]$ which is sent to $\preinv (\phi(g))$ in $\princ H=\princ H$ which corresponds to $\phi(g):\USymH$ under $\pathsp{}^H$.  In other words, $AB(\phi,!)=(\phi,!)$.  The composite $BA$ is similar.
\end{proof}

\section{Actions}
\label{sec:Gsetsabstrconcr}
\marginnote{Recall from \cref{def:abstrGtorsors} that the type of $\abstr(G)$-sets is
  $$\absGSet[\abstr(G)]\defequi \sum_{\absGSetvar:\Set}\absHom({\abstr(G)},\abstr(\Sigma_{\absGSetvar})).$$}

Given a group $G$ it should by now come as no surprise that the type of $G$-sets is equivalent to the type of $\abstr(G)$-sets.
According to \cref{lem:homomabstrconcr}
$$\abstr:\Hom(G,\Sigma_{\absGSetvar})\to\absHom(\abstr(G),\abstr(\Sigma_{\absGSetvar}))$$
is an equivalence, where the group $\Sigma_{\absGSetvar}$ (as a pointed connected groupoid) is the component of the groupoid $\Set$, pointed at $\absGSetvar$.  The component information is moot since we're talking about pointed maps from $\BG$ and we see that $\Hom(G,\Sigma_{\absGSetvar})$ is equivalent to $\sum_{F:\BG_\div\to\Set}(\absGSetvar=F(\sh_G))$.  Finally,
$$\mathrm{pr}:\sum_{\absGSetvar}\sum_{F:\BG_\div\to\Set}(\absGSetvar=F(\sh_G))\we
(\BG_\div\to\Set),\quad \mathrm{pr}(\absGSetvar,F,p)\defequi F
$$
is an equivalence (since $\sum_{\absGSetvar}(\absGSetvar=F(\sh_G))$ is contractible).
Backtracking these equivalences we see that we have established
\begin{lemma}
  \label{lem:actionsconcreteandabstract}
  Let $G$ be a group.  Then the map
  $$\ev_{\sh_G}:\GSet\to\absGSet[\abstr(G)],\qquad \ev_{\sh_G}(X)\defequi(X(\sh_G),a_X)
$$
is an equivalence, where the homomorphism $a_X:\absHom(\abstr(G), \abstr(\Sigma_{X(\sh_G)}))$ is given by transport $X:\USymG\defequi(\sh_G\eqto \sh_G)\to (X(\sh_G)=X(\sh_G))$.
\end{lemma}
If $X$ is a $G$-set, $g:\USymG$ and $x:X(\sh_G)$, we seek forgiveness for writing $g\cdot x:X(\sh_G)$ instead of $\cast(a_X(g))(x)$.\footnote{and I ask forgiveness for strongly disliking the use of ``$\cast$'' as a name for some tacitly understood map!}

\begin{example}
  \label{ex:abstrandconj}
  Let $H$ and $G$ be groups.  Recall that the set of homomorphisms from $H$ to $G$ is a $G$-set in a natural way:
$$\Hom(H,G):\BG\to\Set,\quad \Hom(H,G)(y)\defequi \sum_{F:\BH_\div\to \BG_\div}(y=F(\sh_H)).$$

What abstract $\abstr(G)$-set does this correspond to?
In particular, under the equivalence $\abstr:\Hom(H,G)\to\absHom(\abstr(H),\abstr(G))$, what is the corresponding action of $\abstr(G)$ on the abstract homomorphisms?

The answer is that $g:\USymG$ acts on $\absHom(\abstr(H),\abstr(G))$ by postcomposing with conjugation $\conj^g$ by $g$ as defined in \cref{ex:conjhom}.

Let us spell this out in some detail:
If $(F,p):\Hom(H,G)(\sh_G)\defequi
 \sum_{F:\BH_\div\to \BG_\div}(\sh_G\eqto F(\sh_H))$ and $g:\USymG$, then $g\cdot(F,p)\defequi(F,p\,g^{-1})$.  If we show that the action of $g$ sends $\abstr(F,p)$ to $\conj^g\circ\abstr(F,p)$ we are done.

Recall that $\abstr(F,p)$ consists of the composite
$$\xymatrix{\USymH\ar[r]^-{F^=}&(F(\sh_H)=F(\sh_G))\ar[rr]^-{t\mapsto p^{-1}t\,p}&&\USymG},$$
(\ie $\abstr(F,p)$ applied to $q:\USymH $ is  $p^{-1}F^=(q)\,p$)  together with the proof that this is an abstract group homomorphism.
We see that $\abstr(F,p\,g^{-1})$ is given by conjugation:
$q\mapsto(p\,g^{-1})^{-1}F^=(q)\,(p\,g^{-1})=g\,(p^{-1}F^=(q)\,p)\,g^{-1}$, or in other words $\conj^g\circ\abstr(F,p)$.
\end{example}
For reference we list the conclusion of this example as a lemma:
\begin{lemma}\label{lem:abstrandconj}
  If $H$ and $G$ are groups, then the equivalence of \cref{lem:actionsconcreteandabstract} sends the $G$-set $\Hom(H,G)$ to the $\abstr(G)$-set $\absHom(\abstr(H),\abstr(G))$ with action given by postcomposing with conjugation by elements of $\abstr(G)$.
\end{lemma}

If $f:\Hom(G,G')$ is a homomorphism, then precomposition with $\Bf:\BG\to \BG'$ defines a map $$f^*:(G'\text{-}\Set)\to(G\text{-}\Set).$$
\marginnote{Recall that \cref{lem:eq-mono-cover} told us that $f$ is an epimorphism precisely when $\USymf$ is a surjection.}
We will have the occasion to use the following result which essentially says that if $f:\Hom(G,G')$ is an epimorphism, then $f^*$ embeds the type of $G'$-sets as some of the components of the type of $G$-sets.
\begin{lemma}
  \label{lem:epifullyfaithful}
  Let $G$ and $G'$ be groups and let $f:\Hom(G,G')$ be an epimorphism.
  Then the map $f^*:(G'\text{-}\Set)\to(G\text{-}\Set)$ (induced by precomposition with $\Bf:\BG\to \BG'$) is ``fully faithful'' in the sense that if $X,Y$ are $G'$-sets, then
$$f^*:(X=Y)\to(f^*X=f^*Y)
$$
is an equivalence.
\end{lemma}
\begin{proof}
  Evaluation at $\sh_G$  yields an injective map
$$\mathrm{ev}_{\sh_G}:(f^*X=f^*Y)\to(X(f(\sh_G)=Y(f(\sh_G)))$$ and the composite
$$\mathrm{ev}_{\sh_G}f^*=\mathrm{ev}_{f(\sh_G)}:(X=Y)\to(X(f(\sh_G)=Y(f(\sh_G)))$$
 is the likewise injective, so $f^*:(X=Y)\to(f^*X=f^*Y)$ is injective.

For surjectivity, let $F':f^*X=f^*Y$ and write, for typographical convenience, $a:X(f(\sh_G)=Y(f(\sh_G))$ for $\mathrm{ev}_{\sh_G}F'\defequi F'_{\sh_G}$.
By the equivalence between $G$-sets and $\abstr(G)$-sets, $F'$ is uniquely pinned down by $a$ and the requirement that for all $g'=f(g)$ with $g:\USymG$ the diagram
$$\xymatrix{X(f(\sh_G))\ar@{=}[r]^{X({g'})}\ar@{=}[d]_{a}&
  X(f(\sh_G))\ar@{=}[d]_{a}\\
  Y(f(\sh_G))\ar@{=}[r]^{Y({g'})}&Y(f(\sh_G))}
$$
commutes.  Likewise, (using transport along the identity $p_f:\sh_{G'}=f(\sh_G)$) an $F:X=Y$ in the preimage of $a$ is pinned down by the commutativity of the same diagram, but with $g':f(\sh_G)=f(\sh_G)$ arbitrary (an a priori more severe requirement, again reflecting injectivity).   However, when $f:\USymG\to\USymG'$ is surjective these requirements coincide, showing that $f^*$ is an equivalence.


% Fix for the moment an  $a:X(f(\sh_G)=Y(f(\sh_G))$

% Now, by transport along the identity $p_f:\sh_{G'}=f(\sh_G)$ and the equivalence between $G'$-sets and $\abstr(G')$-sets, an identity $F':X=Y$ of $G'$-sets is uniquely pinned down by an identity $F'_{f(\sh_G)}:X(f(\sh_G)=Y(f(\sh_G))$ together with the proposition that for all $g':f(\sh_G)=f(\sh_G)$ the diagram $$\xymatrix{X(f(\sh_G))\ar@{=}[r]^{X_{g'}}\ar@{=}[d]_{F'_{f(\sh_G)}}&
%   X(f(\sh_G))\ar@{=}[d]_{F'_{f(\sh_G)}}\\
%   Y(f(\sh_G))\ar@{=}[r]^{Y_{g'}}&Y(f(\sh_G))}
% $$
% commutes.  Likewise, an identity $F:f^*X=f^*Y$ is given by exactly the same data, except that the diagram is only required to commute for $g'=f(g)$ for all $g:\USymG$.  But when $f:\USymG\to\USymG'$ these requirements coincide.


% ; $F:X=Y$ is in the preimage of $a:X(f(\sh_G)=Y(f(\sh_G))$ if and only if $a=F_{f(\sh_G)}$ and for all $g':f(\sh_G)=f(\sh_G)$ the diagram
% $$\xymatrix{X(f(\sh_G))\ar@{=}[r]^{X_{g'}}\ar@{=}[d]_{F_{f(\sh_G)}}&
%   X(f(\sh_G))\ar@{=}[d]_{F_{f(\sh_G)}}\\
%   Y(f(\sh_G))\ar@{=}[r]^{Y_{g'}}&Y(f(\sh_G))}
% $$
% commutes.  However, since $f$ is surjective there is a $g:\USymG$ so that $g'=f(g)$.  Therefore, anything in $f^*X=f^*Y$ which is in the preimage of $a$ is in the image of $f^*:X=Y$ and we have shown that $f^*$ is also a surjection.
\end{proof}

\begin{remark}
  \label{rem:inducedGsetfromabstracthomomorphisms} \MB{From 5.5, move to fit.}
  Notice that our construction of the induced $G$-set works equally well for
  a homomorphism of abstract groups $\phi:\absHom(\abstr(G),\abstr(H))$:
  if $X:\BG\to\Set$ is a $G$-set, then we can
  define the $H$-set $\phi_*X:\BH\to\Set$ by
  \[
    \phi_*X(y)\defequi (\sh_H \eqto y) \times_G X(\sh_G)
  \]
  to be the set quotient of $(\sh_H\eqto y)\times X(\sh_G)$ by
  the relation
  $(p,x)\sim(p\, \phi(q)^{-1},q\cdot x)$ for all $q:\sh_G\eqto\sh_G$.
  Just as above, for $X$ the principal $G$-torsor we get an identity
  $\eta_\phi:\phi_*\princ G \eqto \princ H$ which, when evaluated at $y:\BH$,
  corresponds under univalence to the equivalence
  \[
    (\sh_H\eqto y)\times_G\USymG\equivto (\sh_H\eqto y)
  \]
  sending $[(p,q)]$ to $p\,\phi(q):(\sh_H\eqto y)$.
\end{remark}

\section{Heaps \texorpdfstring{$(\dagger)$}{(\textdagger) \color{red} just moved from symmetry without proofreading BID211116}}
\label{sec:heaps}

Recall that we in \cref{rem:heap-preview} wondered about
the status of general identity types $a\eqto_A a'$,
for $a$ and $a'$ elements of a groupoid $A$,
as opposed to the more special loop types $a\eqto_Aa$.\marginnote{%
  This section has no implications for the rest of the book,
  and can thus safely be skipped on a first reading.}
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 \eqto_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 \emph{two} equivalences $l,r:\Heap \equivto \sum_{G:\Group}\BG$,
  and one $c:\Group \equivto \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}


%%% Local Variables:
%%% mode: LaTeX
%%% fill-column: 144
%%% latex-block-names: ("lemma" "theorem" "remark" "definition" "corollary" "fact" "properties" "conjecture" "proof" "question" "proposition" "exercise")
%%% TeX-master: "book"
%%% TeX-command-extra-options: "-fmt=macros"
%%% compile-command: "make book.pdf"
%%% End: