§ INTRODUCTION

Predicting future environmental change provides many benefits. A microbe gains by anticipating the availability of sugars. A plant gains by forecasting the flow of nutrients. Plasticity benefits from a head start on altering physiology or form. Competitive players profit by preparing for the next step in a contest pigliucci01phenotypic,dewitt04phenotypic,kussell05phenotypic,mitchell09adaptive,reed10phenotypic,shemesh10anticipating,goo12bacterial,siegal15shifting,venturelli15population,21phenotypic.

Organisms often anticipate regular patterns of change, such as circadian rhythms or seasonal cycles. However, many regularities arise as stochastic trends. To take advantage of such trends, a biological circuit must measure past directionality and use that measurement to predict the direction of future change.

In the literature, studies of E. coli chemotaxis develop the most compelling models for the anticipation of trend tu08modeling,shimizu10amodular,alon19an-introduction. Cells measure changes in chemical concentrations to predict whether future changes will be increasing or decreasing. Tjalma et al.'s tjalma23trade-offs excellent recent article synthesizes past literature and develops new models.

This article introduces a simple model for anticipating trend. Roughly speaking, the model estimates the momentum of the current trend by the difference between a shorter-term moving average and a longer-term moving average. That estimate of momentum predicts the future direction of change because the future trend often continues in the direction of the current momentum.

Most existing models, such as those for E. coli chemotaxis, also base predictions on estimates of current or past trend. However, those previous models typically add specific aspects of a particular application or additional complexities, such as noise filtering. Those additions are interesting but also obscure the simplicity and generality of the underlying way in which estimates of momentum anticipate future trend.

The model here strips nonessential features to emphasize the fundamental structure of anticipation for simple stochastic trends. That abstraction provides the basis for future applications across a broader range of biological problems.

Empirically, the model predicts the primary mechanism that organisms use to anticipate environmental trends and the pattern of anticipatory response to environmental changes. Theoretically, the model provides the foundation for developing further predictions about tradeoffs between rapid adjustment of anticipated environmental changes and the susceptibility to perturbation of the circuit that predicts trends tjalma23trade-offs.

The model's simplicity also reveals a close connection to the moving average convergence-divergence (MACD) indicator, the most widely used measure of momentum and trend to analyze asset prices in financial time series murphy99technical,schwager99getting,pring14technical. That connection between biological models and financial analysis encourages application of the highly developed models of information and anticipation in finance to biological problems.

§ THE CHALLENGE

Let $u_t$ be a randomly varying input signal. We wish to predict the direction of change at a future time, $t+1$, relative to the current time, $t$, which means predicting the sign of $\GD u_t = u_{t+1}-u_t$. If $u$ changes in a purely random way, as a random walk with no directionality, then expected prediction success above $1/2$ is not possible. For prediction to be possible, we must assume some pattern to the fluctuations in $u_t$.

An exponential moving average of purely random inputs is perhaps the most generic type of trend. Start with a random walk, $\hat{u}_t$, sampled at discrete times, $t=0,1,\dots$. Then replace each value at time $t$ by its exponential moving average, $u_t = (1-\Gd) \hat{u}_t + \Gd u_{t-1}$. The value of $0\le\Gd\le1$ sets the memory scale, with larger values averaging over longer time periods. Here, we linearly interpolate between the discretely sampled points to obtain values of $u_t$ continuously with time.

The future change in $u_t$ is positive when

\begin{equation}\label{eq:ema}
\GD u_t = (1-\Gd)\GD\hat{u}_t + \Gd\GD u_{t-1} > 0.
\end{equation}

Because $\hat{u}_t$ is a random walk, its change is equally likely to be positive or negative. Thus, the best prediction for the sign of $\GD u_t$ is the sign of $\GD u_{t-1}$. In other words, the most recently observed direction of change provides the best prediction for the next direction of change.

Roughly speaking, we may think of the currently observed change, $\GD u_{t-1}$, as the trend momentum. Positive momentum means that the trend is likely to continue up. Negative momentum means that the trend is likely to continue down.

The greater the momentum, the more likely the trend will continue in the same direction. For example, the larger $\GD u_{t-1}$, the more negative the underlying random walk change, $\GD\hat{u}_t$, must be to reverse the trend. Increasingly extreme moves in the underlying random walk are increasingly uncommon.

Thus, an ideal internal model uses the currently observed trend direction to predict the next direction of change. And it uses the trend momentum to estimate the confidence in the directional prediction.

§ EXPONENTIAL MOVING AVERAGE

I claimed that an exponential moving average provides a common type of trend. I made that claim because any process that balances a fluctuating input against a steady decay describes an exponential moving average. For example, the differential equation

\begin{equation*}
\dot{z} = u - \Gl z
\end{equation*}

determines a level of $z$ that balances production or input, $u$, against steady decay at rate $\Gl$. With $u_0=0$, the value of $z$ at time $t$ is

\begin{equation*}
z(t) = \int_0^t e^{-\Gl(t-\Gt)}u(\Gt)\dd\Gt,
\end{equation*}

which is proportional to the continuous time exponential moving average of $z$ at that time. The process in ema is a discrete time version of the balance between input and decay.

§ THE CIRCUIT

To predict the trend direction, the following circuit calculates the difference between two moving averages, each average taken over a different time scale

\begin{align}\label{eq:cellTrend}
\begin{split}
\dot{x}&=\Ga u - \Gb x\\
\dot{y}&=\Gg\lr{\Ga u - \Gb y}.
\end{split}
\end{align}

Overdots denote derivatives with respect to time, $t$, and $x,y,u$ are functions of time.
For constant input, $u$, the molecular of abundances of $x$ and $y$ have the same equilibrium values, $\Ga/\Gb$. As the input, $u$, changes, $y$ changes more slowly than $x$ when $\Gg < 1$. Thus, $x-y$ tends to be positive when $u$ is increasing and negative when $u$ is decreasing. The values of $x$ and $y$ are approximately proportional to shorter and longer exponential moving averages of the input, $u$.

§ AN EXAMPLE

We can optimize the parameters relative to a particular goal. Figure 1 shows an example of an optimized circuit that predicts the future direction of change in $u_t$. Define maximum potential accuracy as the frequency at which the prior sign of change in $u_t$ predicts the next sign of change, a continuation of trend.

In Fig. 1, the maximum potential accuracy is $0.8$. Stochasticity in the input sequence means that sometimes the sign of the prior difference does not match the direction of the next difference. For this example, the optimized circuit accuracy is close the maximum potential accuracy, with a median deviation from the maximum of $0.001$.

Figure 1b shows the classic MACD pattern for trend prediction from financial analysis. The slower signal in gold, which is the variable $y$, lags the faster signal in blue, which is the variable, $x$. A predicted trend reversal arises when the fast blue signal crosses the slow gold signal, that is, when the sign of $x-y$ changes. Figure 1c traces a function of the $x-y$ difference.

A convergence between the trends in panel b and c predicts a continuation of the current trend. A divergence between the trends in the two panels foreshadows a potential upcoming change in direction for the trend.

For example, starting at time point 98, the $x-y$ difference begins to shrink, causing an upturn in the trend in panel c. That uptrend signals a slowing of the downward momentum. At first the actual trend in panel b continues downward. Thus, the trends in the two panels are diverging. Then, at time point 104, the actual trend in b turns up, a convergence with the trend in c, signaling the potential start of an upswing, which in fact does occur.

Typically, a change in momentum (panel c) precedes a change in trend (panel b), as happens around time point 104. The reason a slowing of momentum typically precedes a change in trend can be seen in ema, which shows how changes in the direction of an exponentially smoothed input are often dominated by the momentum term. However, when the trend changes abruptly, momentum does not precede trend, as happends around time point 92.

§ ACCURACY VERSUS ROBUSTNESS

High accuracy requires that the $x-y$ predictor in Fig. 1c switches sign immediately when the input turns down. The input appears as the red line in Fig. 1a. To achieve high accuracy in forecasting a change in trend direction, in Fig. 1b, the slower moving average, $y$, in gold, must remain close to the faster moving average, $x$, in blue.

The small difference between the moving averages, $x$ and $y$, means that false signals can arise from small perturbations. For example, at time point 102 in Fig. 1b, the moving averages touch, predicting an imminent reversal that does not subsequently occur. In addition, noise in the state variables $x$ and $y$ can trigger false signals.

Figure 2 shows the circuit optimized for wider differences between the fast and slow moving averages, $x$ and $y$. In panel b, The wider differences provide a stronger signal during a trend but lag in giving a signal when the trend does change direction. This system gives fewer false signals and is robust to small perturbations. However, because it lags when the trend does change, it has a lower accuracy when using the sign of the current difference, $x-y$, to predict the direction of change in the input in the next time period. The median deviation from the maximum accuracy is $0.12$, compared with a deviation of $0.001$ in the circuit illustrated in Fig. 1.

In general, systems can be tuned to balance various tradeoffs, such as accuracy versus robustness murphy99technical,schwager99getting,pring14technical,tjalma23trade-offs.

Prediction for the direction of change in a sequence of observations. Dynamics given by cellTrend. In this example, the parameters $\Ga,\Gb,\Gg$ were optimized for accuracy of prediction, yielding $0.1663,0.08314,0.2782$, respectively. The plots show a subset of time points to magnify patterns and make them easier to see. (a) The faster of the two moving averages, $x$, in blue, tracks the input sequence, $u_t$, in red. (b) The fast and slow moving averages, $x$ and $y$, in blue and gold, respectively. (c) The difference between the moving averages, plotted as $1000[\Gs(x-y)-0.5]$, in which $\Gs(z)=e^z\large/\large(1+e^z\large)$ is the sigmoid function. The sign predicts the direction of change in the next time step. The magnitude reflects the momentum, a measure of the relative confidence in the prediction for the future direction of change. To calculate the input sequence in ema, the random walk follows a Wiener process with mean $0$ and standard deviation $0.2$, and the exponential moving average memory parameter is $\Gd=0.2$. For each realized sequence of the random walk, the values are normalized to $[0.25,0.75]$ by affine transformation, yielding $\hat{u}$. The timescale and abundances in the plots have arbitrary units. The freely available computer code describes the scaling of time, the parameters, the optimization, and the production of graphics steven_a_frank_2024_10967108.

Tradeoff between accuracy and robustness. Same plots as Fig. 1 but with slower moving averages. Optimized parameters $\Ga,\Gb,\Gg$ are $0.4179,0.009483,0.2587$.

§ CONCLUSION

Prior models analyzed how biochemical circuits predict future environmental changes tu08modeling,shimizu10amodular,alon19an-introduction,mitchell09adaptive,becker15optimal,tjalma23trade-offs. Those models use recent differences in input to predict future changes because that is the essential nature of the problem.

Although the prior models described biological circuits that predict environmental changes, none of those prior analyses presented a circuit and an explanation as simple as those given here. In essence, the difference between a shorter, more immediate moving average, $x$, and a longer, slower moving average, $y$, provides the basis to forecast trends.

In the technical analysis of financial prices, the MACD indicator for moving average convergence-divergence is calculated as the difference between longer and shorter moving averages. Organisms may use a similar calculation to anticipate environmental trends.

§ AUTHOR CONTRIBUTIONS

SAF did everything.

§ ACKNOWLEDGMENTS

The Donald Bren Foundation, US Department of Defense grant W911NF2010227, and US National Science Foundation grant DEB-2325755 support my research.

§ SUPPLEMENTAL INFORMATION

Software code and output for all analyses and figures available at GitHub steven_a_frank_2024_10967108.


École Normale Supérieure de<EMAIL_ADDRESS>LIX, CNRS, École
polytechnique, Institut Polytechnique de Paris, 91120 Palaiseau,
France.samuel.mimram@polytechnique.eduhttps://orcid.org/0000-0002-0767-2569
LIX, CNRS, École polytechnique, Institut Polytechnique de Paris, 91120
Palaiseau,
France.emile.oleon@polytechnique.eduhttps://orcid.org/0009-0001-8398-2577
Camil Champin, Samuel Mimram and Émile Oleon [500]Theory of computation
Constructive mathematics [subcategory=Proofs, cite=,
swhid=]Softwarehttps://github.com/smimram/generated-deloopings-agda Jakob
Rehof 1 9th International Conference on Formal Structures for Computation and
Deduction (FSCD 2024) FSCD 2024 FSCD 2024 July 10-13, 2024 Tallinn, Estonia
299 3

# Delooping generated groups in homotopy type theory

Camil Champin  Samuel Mimram  Émile Oleon

###### Abstract

Homotopy type theory is a logical setting based on Martin-Löf type theory in
which one can perform geometric constructions and proofs in a synthetic way.
Namely, types can be interpreted as spaces (up to continuous deformation) and
proofs as homotopy invariant constructions. In this context, loop spaces of
pointed connected groupoids provide a natural representation of groups, and
any group can be obtained as the loop space of such a type, which is then
called a _delooping_ of the group. There are two main methods to construct the
delooping of an arbitrary group $G$. The first one consists in describing it
as a pointed higher inductive type, whereas the second one consists in taking
the connected component of the principal $G$-torsor in the type of sets
equipped with an action of $G$. We show here that, when a presentation is
known for the group, simpler variants of those constructions can be used to
build deloopings. The resulting types are more amenable to computations and
lead to simpler meta-theoretic reasoning. We also investigate, in this
context, an abstract construction for the Cayley graph of a generated group
and show that it encodes the relations of the group. Most of the developments
performed in the article have been formalized using the cubical version of the
Agda proof assistant.

###### keywords:

homotopy type theory, delooping, group, generator, Cayley graph

###### category:

## Introduction

Homotopy type theory was introduced around 2010 [27]. It is based on Martin-
Löf type theory [20], starting from the idea that types in logic should be
interpreted not only as sets, as traditionally done in semantics of logic, but
rather as _spaces_ considered up to homotopy. Namely, the identities between
two elements of a type can be thought of as paths between points corresponding
to the elements, identities on identities as homotopies between paths, and so
on. Moreover, this correspondence can be made to work precisely, by
postulating the _univalence axiom_ [14], which states that identities between
types coincide with equivalences. This opens the way to the implementation of
geometric constructions in a synthetic way, by performing operations on types,
which will semantically correspond to the desired operations on spaces. In
this setting, we are interested in providing ways to construct models of
groups which are concise in order to allow for simple proofs, but also to make
the meta-theoretic reasoning easier.

### Delooping groups

Following a well-known construction due to Poincaré at the end of the 19th
century [22], to any type $A$ which is pointed, i.e. equipped with a
distinguished element $\star$, we can associate its _fundamental group_
$\pi_{1}(A):=\|\star=\star\|_{0}$ whose elements are homotopy classes of paths
from $\star$ to itself, with composition given by concatenation and identity
by the constant path. Moreover, when the type $A$ is a groupoid, in the sense
that any two homotopies between paths are homotopic, this fundamental group
coincides with the _loop space_ $\operatorname{\Omega}A:=(\star=\star)$,
defined similarly but without quotienting paths up to homotopy. Once this
observation made, it is natural to wonder whether every group $G$ arises as
the loop space of some groupoid. It turns out that this is the case: to every
group one can associate a pointed connected groupoid type $\operatorname{B}G$,
called its _delooping_ , whose loop space is $G$. Moreover, there is
essentially only one such type, thus justifying the notation.

### Internal and external points of view

The delooping construction, which can be found in various places [2, 5], and
will be recalled in the article, induces an equivalence between the type of
groups and the type of pointed connected groupoids (Theorem B.4). This thus
provides us with two alternative descriptions of groups in homotopy type
theory. The one as (loop spaces of) pointed connected groupoids can be thought
of as an _internal_ one, since the structure is deduced from the types without
imposing further axioms; by opposition, the traditional one as groups (sets
equipped with multiplication and unit operations) is rather an _external_ one
(some also use the terminology _concrete_ and _abstract_ instead of internal
and external [2]). We should also say here that pointed connected types (which
are not necessarily groupoids) can be thought of as higher versions of groups,
where the axioms only hold up to higher identities which are themselves
coherent, and so on.

### Two ways to construct deloopings

Two generic ways are currently known in order to construct the delooping
$\operatorname{B}G$ of a group $G$, which we both refine in this article. The
first one is a particular case of the definition of _Eilenberg-MacLane spaces_
in homotopy type theory due to Finster and Licata [17]. It consists in
constructing $\operatorname{B}G$ as a higher inductive type with one point (so
that it is pointed), one loop for each element of $G$, one identity for each
entry in the multiplication table of $G$, and then truncating the resulting
type as a groupoid. One can imagine that the resulting space has the right
loop space “by construction”, although the formal proof is non-trivial.

The second one is the _torsor_ construction which originates in algebraic
topology [12] and can be adapted in homotopy type theory [2, 5, 29]. One can
consider the type of _$G$ -sets_, which are sets equipped with an action of
$G$. Among those, there is a canonical one, called the _principal $G$-torsor_
$\operatorname{P}_{G}$, which arises from the action of the group $G$ on
itself by left multiplication. It can be shown that the loop space of the type
of $G$-sets, pointed on the principal $G$-torsor $\operatorname{P}_{G}$, is
the group $G$. Moreover, if one restricts the type of $G$-sets to the
connected component of the principal $G$-torsor, one obtains the type of _$G$
-torsors_, which is a delooping of $G$.

### Smaller deloopings of groups

In this article, we are interested in refining the above two constructions in
order to provide ones which are “simpler” (in the sense that we have less
constructors, or the definition requires to introduce less material), when a
presentation by generators and relation is known for the group.

For the first construction (as a higher inductive type), we show here the we
can construct $\operatorname{B}G$ as the higher inductive type generated by
one point, one loop for each generator of the presentation (as opposed to
every element of the group), one identity for each relation of the
presentation and taking the groupoid truncation (Theorem 3.3). This has the
advantage of resulting in types are simpler to define, require handling less
cases when reasoning with those by induction, and are closer to the usual
combinatorial description of groups. Moreover, we claim that the traditional
methods based on rewriting [13, 1] in order to compute invariants such as
homology or coherence can be applied to those. Namely, a first important step
in this direction was obtained by Kraus and von Raummer’s adaptation of
Squier’s coherence theorem in homotopy type theory [16].

For the second construction (based on $G$-torsors), we show that a simpler
definition can be achieved when a generating set $X$ is known for $G$. Namely,
we show that one can perform essentially the same construction, but replacing
$G$-gets by what we call here $X$-sets (Theorem 5.3), where we only need to
consider the action for the generators (as opposed to the whole group). As an
illuminating example, consider the case $G=\mathbb{Z}$, whose delooping is
known to be the circle $\operatorname{B}\mathbb{Z}=\operatorname{S}^{1}$. The
type $\mathcal{U}^{\circlearrowleft}$ of all endomorphisms, on any type,
contains, as a particular element, the successor function
$s:\mathbb{Z}\to\mathbb{Z}$. Our results imply that the connected component of
$s$ in $\mathcal{U}^{\circlearrowleft}$ is a delooping of $\mathbb{Z}$. This
description is arguably simpler than the one of $\mathbb{Z}$-torsors: indeed,
morphisms of $\mathbb{Z}$-sets are required to preserve the action of every
element of $\mathbb{Z}$, while morphisms in $\mathcal{U}^{\circlearrowleft}$
are only required to preserve the action of $1$ (which corresponds to the
successor). The above description is the one which is used in UniMath in order
to define the circle $\operatorname{S}^{1}$ [3]: the reason why they use it
instead of more traditional one [27] is that they do not allow themselves to
use higher inductive types because those are not entirely clear from a meta-
theoretic point of view (there is no general definition, even though there are
proposals [18], the semantics of type theory [14] has not been fully worked
out in their presence, etc.). Our result thus give an abstract explanation
about why this construction works and provides a generic way to easily define
many more deloopings without resorting to higher inductive types, if one is
not disposed to do so.

### Cayley graphs

As a last aspect of our study of generated groups in homotopy type theory, we
provide here a pleasant abstract description of Cayley graphs, which is a
well-known construction in group theory [9, 19]. We show that, given a group
$G$ with a set $X$ of generators, the Cayley graph can be obtained as the
kernel of the canonical map $\operatorname{B}X^{*}\to\operatorname{B}G$, where
$X^{*}$ is the free group on $X$ (Theorem 6.1). This establishes those graphs
as a measure of the difference between deloopings and their approximations,
and suggests higher dimensional versions of those.

### Formalization

Most of the results presented in this article have been formalized in the
cubical variant of the Agda proof assistant [28] using the “standard library”
which has been developed for it [26]. Our developments are publicly available
[10], and we provide pointers to the formalized results.

### Plan of the paper

We begin by briefly recalling the fundamental notions of homotopy type theory
which will be used throughout the paper (Section 1), as well as the notion of
delooping for a group (Section 2). We first present the construction of
deloopings using higher inductive types, and explain how those can be
simplified when a presentation is known for the group (Section 3). We then
present the other approach for defining delooping of groups based on the
torsor construction (Section 4) and show how it can be simplified when a
generating set is known for the group (Section 5). Finally, we investigate the
construction of Cayley graphs in homotopy type theory (Section 6) and
conclude, presenting possible extensions of this work (Section 7).

### Acknowledgments

We would like to thank Dan Christensen as well as an anonymous reviewer for
useful comments on early drafts of this article.

##  1 Homotopy type theory

We unfortunately do not have enough space here to provide an introduction from
scratch to dependent type theory and homotopy type theory, so we refer the
reader to the reference book for an in depth presentation [27]. The main
purpose of this section is to fix some terminology and notations for classical
notions.

### Universe

We write $\mathcal{U}$ for the _universe_ , i.e. the large type of all small
types, which we suppose to be closed under dependent sums and products. We
write $\Pi(x:A).B$ or $(x:A)\to B$ for $\Pi$-types, and $A\to B$ for the case
where $B$ is non-dependent. Similarly, we write $\Sigma(x:A).B$ for
$\Sigma$-types, and $A\times B$ for the non-dependent version. The two
projections from a $\Sigma$-type are respectively written $\pi$ and
$\pi^{\prime}$.

### Paths

Given a type $A:\mathcal{U}$ and two elements $a,b:A$, we write $a=_{A}b$ for
the type of _identities_ , or _paths_ , between $a$ and $b$: its elements are
proofs of equality between $a$ and $b$. In particular, for any $a:A$, the type
$a=a$ contains the term $\operatorname{refl}_{a}$ witnessing for reflexivity
of equality. We sometimes write $x:=t$ to indicate that $x$ and $t$ are equal
by definition. The elimination principle of identities, aka  _path induction_
and often noted $J$, roughly states that, given $a:A$, in order to show a
property $P:(x:A)\to(a=x)\to\mathcal{U}$ for every $x:A$ and $p:a=x$ it is
enough to show it in the case where $x:=a$ and $p:=\operatorname{refl}_{a}$.
By path induction, the following can be shown. Given a type $A$ and a type
family $B:A\to\mathcal{U}$, a path $p:x=y$ in $A$ induces a function
$B^{\to}_{p}:B(x)\to B(y)$ witnessing for the fact that equality is
_substitutive_. As a special case, any path $p:A=B$ between two types
$A,B:\mathcal{U}$ induces a function $p^{\to}:A\to B$, called the _transport_
along $p$, as well as an inverse function $p^{\leftarrow}:B\to A$. Finally,
given a function $f:A\to B$, any path $p:x=y$ in $A$ induces a path
$f^{=}(p):f(x)=f(y)$ witnessing for the fact that equality is a _congruence_.

### Higher inductive types

Many functional programming languages allow the definition of inductive types,
which are freely generated by constructors. For instance, the type
$\operatorname{S}^{0}$ of booleans is generated by two elements (true and
false). In the context of homotopy type theory, languages such as cubical Agda
feature a useful generalization of such types, called _higher inductive
types_. They allow, in addition to traditional constructors for elements of
the type, constructors for equalities between elements of the type. For
instance, the type corresponding to the circle $\operatorname{S}^{1}$ can be
defined as generated by two points $a$ and $b$ and two equalities $p,q:a=b$
between those points. Higher-dimensional spheres $\operatorname{S}^{n}$ can be
defined in a similar way.

### Univalence

A map $f:A\to B$ is an _equivalence_ when it admits both a left and a right
inverse. In particular, every isomorphism is an equivalence. We write $A\simeq
B$ for the type of equivalences from $A$ to $B$. The identity is clearly an
equivalence and we thus have, by path induction, a canonical map
$(A=B)\to(A\simeq B)$ for every types $A$ and $B$: the _univalence axiom_
states that this map is itself an equivalence. In particular, every
equivalence $A\simeq B$ induces a path $A=B$. It is known that univalence
implies the _function extensionality_ principle [27, Section 2.9]: given
functions $f,g:A\to B$, if $f(x)=g(x)$ for any $x:A$ then $f=g$ (and the
expected generalization to dependent function types is also valid).

### Homotopy levels

A type $A$ is _contractible_ when the type $\Sigma(x:A).(y:A)\to(x=y)$ is
inhabited: this means that we have a “contraction point” $a_{0}:A$, and a
continuous family of paths from $a_{0}$ to every other point in $A$. A type
$A$ is a _proposition_ (resp. a _set_ , resp. a _groupoid_) when $(x=y)$ is
contractible (resp. a proposition, resp. a set) for every $x,y:A$.
Intuitively, a contractible type is a point (up to homotopy), a proposition is
a point or is empty, a set is a collection of points and a groupoid is a space
which bears no non-trivial 2-dimensional (or higher) structure. We write
$\operatorname{Set}$ for the type of sets. Given a type $A$, we write
$\operatorname{isSet}(A)$ (resp. $\operatorname{isGroupoid}(A)$) for the
predicate indicating that $A$ is a set (resp. groupoid).

### Truncation

Given a type $A$, its _propositional truncation_ turns it into a proposition
in a universal way. It consists of a type $\|A\|_{-1}$, which is a
proposition, equipped with a map $|-|_{-1}:A\to\|A\|_{-1}$ such that, for any
proposition $B$, the map $(\|A\|_{-1}\to B)\to(A\to B)$ induced by
precomposition by $|-|_{-1}$ is an equivalence. Intuitively, the type
$\|A\|_{-1}$ behaves like $A$, except that we do not have access to its
individual elements: the elimination principle for propositional truncation
states that in order to construct an element of $B$ from an element of
$\|A\|_{-1}$, we can only assume that we have an element of $A$ if $B$ itself
is a proposition. The _set truncation_ $\|A\|_{0}$ of a type $A$ is defined
similarly, as the universal way of turning $A$ into a set, and we write
$|x|_{0}$ for the image of $x:A$ in the truncation; and we can similarly
define the _groupoid truncation_ $\|A\|_{1}$.

### Fibers

Given a function $f:A\to B$, we write $\operatorname{fib}_{f}b$ for the type
$\Sigma(a:A).(f\,a=b)$, called the _fiber_ of $f$ at $b$. The function $f$ is
said to be _surjective_ when the type
$(b:B)\to\|\operatorname{fib}_{f}b\|_{-1}$ is inhabited, i.e. when every
element of $B$ merely admits a preimage.

##  2 Delooping groups

### The external point of view

A _group_ consists of a set $A$, together with an operation $m:A\to A\to A$
(the _multiplication_), an element $e:A$ (the _unit_), and an operation
$i:A\to A$ (the _inverse_) such that multiplication is associative, admits $e$
as unit, and $i(x)$ is the two-sided inverse of any element $x:A$. We write
$\operatorname{Group}$ for the type of all groups, and
$G\to_{\operatorname{Grp}}H$ for the type of group morphisms between groups
$G$ and $H$. In the following, we use the traditional notations for groups:
given two elements $x,y:G$, we simply write $xy$ instead of $m(x,y)$, $1$
instead of $e$, and $x^{-1}$ instead of $i(x)$.

### The internal point of view

A _pointed_ type consists of a type $A$ together with a distinguished element,
often written $\star$ and sometimes left implicit. Given a pointed type
$(A,\star)$, its _loop space_ $\operatorname{\Omega}A$ is defined as the type
of paths from $\star$ to itself: $\operatorname{\Omega}A:=(\star=\star)$. The
elements of this type are called _loops_. By path induction one can construct,
for every two paths $p:a=b$ and $q:b=c$, a path in $a=c$ called their
_concatenation_ and written $p\cdot q$. Similarly, every path $p:a=b$, admits
an _inverse_ path $p^{-}:b=a$. When $A$ is a pointed groupoid,
$\operatorname{\Omega}A$ is a set, and these operations canonically equip this
set with a structure of group [27, Section 2.1].

### Delooping groups

A _delooping_ of a group $G$ is a pointed connected groupoid
$\operatorname{B}G$ together with an identification
$\operatorname{d}_{G}:\operatorname{\Omega}\operatorname{B}G=G$ (we recall
that a type $A$ is _connected_ when the type $\|A\|_{0}$ is contractible, i.e.
$A$ has one connected component). The notation is justified by the fact that
deloopings are unique. For instance, it is known that the circle is a
delooping of $\mathbb{Z}$: indeed, $\operatorname{S}^{1}$ is a connected
groupoid, and its fundamental group is $\mathbb{Z}$ [27, Section 8.1].

##  3 Delooping using higher inductive types

### Delooping as a higher inductive type

Given a group $G$, its delooping should have a point $\star$ and a loop for
every element of the group. Moreover, we should ensure that the multiplication
of $G$ coincides with the concatenation operation on the loop space, and that
the type we obtain is a (pointed connected) groupoid. This suggests
considering a higher inductive type, noted $\operatorname{K}(G,1)$, with the
following constructors

$\begin{array}[]{l@{\ :\ }l}\star&{\operatorname{K}(G,1)}\\\
\operatorname{\textsf{{loop}}}&G\to\star=\star\\\ \operatorname{\textsf{{loop-
comp}}}&(x,y:G)\to\operatorname{\textsf{{loop}}}x\cdot\operatorname{\textsf{{loop}}}y=\operatorname{\textsf{{loop}}}(xy)\\\
\operatorname{\textsf{{trunc}}}&\operatorname{isGroupoid}(\operatorname{K}(G,1))\end{array}$

This construction was first proposed by Finster and Licata. They also showed,
using the encode-decode method, that it is a delooping of the original group,
i.e. $\operatorname{\Omega}\operatorname{K}(G,1)=G$, see [17, Theorem 3.2].
Note that we only ask here that $\operatorname{\textsf{{loop}}}$ preserves
multiplication (with $\operatorname{\textsf{{loop-comp}}}$), because it can be
shown that this implies preservation of unit and inverses. In particular,
preservation of unit (see EM.loop-id) renders superfluous one of the
constructors present in the original definition [17].

In the following, we will define a variant of this higher inductive type when
the group $G$ is presented, which is smaller and gives rise to computations
closer to traditional group theory.

### Presentations of groups

Given a set $X$, we write $X^{*}$ for the _free group_ over $X$ [27, Theorem
6.11.6]. There is an inclusion function $\iota:X\to X^{*}$ which, by
precomposition, induces an equivalence between morphisms of groups $X^{*}\to
G$ and functions $X\to G$. We write $f^{*}:X^{*}\to G$ for the group morphism
thus induced by a function $f:X\to G$. The elements of $X^{*}$ can be
described as formal composites $a_{1}\ldots a_{n}$ where each $a_{i}$ is an
element of $X$ or a formal inverse of an element of $X$ (such that an element
with an adjacent formal inverse cancel out).

Any free group $X^{*}$ admits a delooping as a wedge of an $X$-indexed familly
of circles. The corresponding type $\bigvee_{X}\operatorname{S}^{1}$ can be
described as the coequalizer

${X}$${1}$${\bigvee_{X}\operatorname{S}^{1}}$ (1)

or, equivalently, as the higher inductive type generated by the two
constructors $\star:\bigvee_{X}\operatorname{S}^{1}$ and
$\operatorname{\textsf{{loop}}}:X\to\star=\star$.

######  Proposition 3.1.

We have $\operatorname{\Omega}\bigvee_{X}\operatorname{S}^{1}=X^{*}$, i.e. the
above type is a $\operatorname{B}X^{*}$.

######  Proof 3.2.

The fact that $\bigvee_{X}\operatorname{S}^{1}$ is a delooping of $X^{*}$ is
not too difficult to show when $X$ has decidable equality, see [27, Exercise
8.2] and [15], but the general case is more involved and was recently proved
in [30]: the main issue is to show that this type is a groupoid.

A group _presentation_ $\langle X\ |\ R\rangle$ consists of a set $X$ of
_generators_ , a set $R$ of _relations_ , and two functions
$\pi,\pi^{\prime}:R\to X^{*}$ respectively associating to a relation its
_source_ and _target_. We often write $r:u\Rightarrow v$ for a relation $r$
with $u$ as source and $v$ as target. Given such a presentation $P$, the
corresponding _presented_ group $[P]$ is the set quotient $X^{*}/R$ of the
free group on $X$ under the smallest congruence identifying the source and the
target of every relation $r:R$. This type can be described as the type
$[P]:=\|{X^{*}}\mathop{\\!/\\!\\!/\\!}R\|_{0}$ obtained by taking the set
truncation of the coequalizer

${R}$${X^{*}}$${X^{*}\mathop{\\!/\\!\\!/\\!}R}$$\scriptstyle{\pi}$$\scriptstyle{\pi^{\prime}}$$\scriptstyle{\kappa}$

From this also follows a description of $[P]$ as a higher inductive type:

$\begin{array}[]{l@{\ :\ }l}\operatorname{\textsf{{word}}}&X^{*}\to[P]\\\
\operatorname{\textsf{{rel}}}&(r:R)\to\operatorname{\textsf{{word}}}(\pi(r))=\operatorname{\textsf{{word}}}(\pi^{\prime}(r))\\\
\operatorname{\textsf{{trunc}}}&\operatorname{isSet}([P])\end{array}$

### A smaller delooping

Suppose given a group $G$ along with a presentation $P:=\langle X\ |\
R\rangle$, i.e. such that $G=[P]$. We define the type $\operatorname{B}P$ as
the following higher inductive type:

$\begin{array}[]{l@{\ :\ }l}\star&{\operatorname{B}P}\\\
\operatorname{\textsf{{gen}}}&X\to(\star=\star)\\\
\operatorname{\textsf{{rel}}}&(r:R)\to(\operatorname{\textsf{{gen}}}^{*}(\pi(r))=\operatorname{\textsf{{gen}}}^{*}(\pi^{\prime}(r)))\\\
\operatorname{\textsf{{trunc}}}&\operatorname{isGroupoid}(\operatorname{B}P)\end{array}$

This type is generated by a point $\star$, then the constructor
$\operatorname{\textsf{{gen}}}$ adds a loop $\underline{a}:\star=\star$ for
every generator $a$, the constructor $\operatorname{\textsf{{rel}}}$ adds an
equality
$\underline{a}_{1}\cdot\underline{a}_{2}\cdot\ldots\cdot\underline{a}_{n}=\underline{b}_{1}\cdot\underline{b}_{2}\cdot\ldots\cdot\underline{b}_{m}$
for each relation $a_{1}\ldots a_{n}\Rightarrow b_{1}\ldots b_{m}$, and the
constructor $\operatorname{\textsf{{trunc}}}$ formally takes the groupoid
truncation of the resulting type. Note that, because of the presence of
$\operatorname{\textsf{{gen}}}^{*}:X^{*}\to(\star=\star)$ in the type of
$\operatorname{\textsf{{rel}}}$, the above inductive type is not accepted as
is in standard proof assistants such as Agda. However, a definition can be
done in two stages, by first considering $\bigvee_{X}\operatorname{S}^{1}$
(i.e. the type generated only by $\star$ and $\operatorname{\textsf{{gen}}}$),
and then defining a second inductive type further quotienting this type (i.e.
adding the constructors $\operatorname{\textsf{{rel}}}$ and
$\operatorname{\textsf{{trunc}}}$), see EM.Delooping. Also, the definition of
$\operatorname{\textsf{{gen}}}^{*}$ requires the group structure on
$\bigvee_{X}\operatorname{S}^{1}$: the group operations are easily defined
from operations on paths (reflexivity, concatenation, symmetry), but the fact
that it is a groupoid is non-trivial (see Proposition 3.1). Our main result in
this section is the following:

######  Theorem 3.3 (EM.theorem).

Given a presentation $P:=\langle X\ |\ R\rangle$, the type $\operatorname{B}P$
is a delooping of the group $[P]$.

######  Proof 3.4.

By induction on $\operatorname{B}P$, we can define a function
$f:\operatorname{B}P\to\operatorname{K}([P],1)$ such that $f\star:=\star$, and
$f(\operatorname{\textsf{{gen}}}a):=\operatorname{\textsf{{loop}}}[a]$ for all
$a:X$. It can be shown that $f$ is then such that
$f^{=}(\operatorname{\textsf{{gen}}}^{*}u)=\operatorname{\textsf{{loop}}}[u]$,
for any $u:X^{*}$. We can therefore define the image $f^{=}(r)$ on a relation
$r:u\Rightarrow v$ as the composite of equalities

$f^{=}(\operatorname{\textsf{{gen}}}^{*}u)=\operatorname{\textsf{{loop}}}[u]=\operatorname{\textsf{{loop}}}[v]=f^{=}(\operatorname{\textsf{{gen}}}^{*}v)$

where the equality in the middle follows from the fact that we have $[u]=[v]$
because of the relation $r$.

In the other direction, the group morphism
$\operatorname{\textsf{{gen}}}^{*}:X^{*}\to\operatorname{\Omega}\operatorname{B}P$
preserves relations (by $\operatorname{\textsf{{rel}}}$), and thus induces a
quotient morphism $g^{\prime}:[P]\to\operatorname{\Omega}\operatorname{B}P$.
We can thus consider the function
$g:\operatorname{K}([P],1)\to\operatorname{B}P$ such that $g(\star)=\star$,
for $x:[P]$ we have $g^{=}(\operatorname{\textsf{{loop}}}x)=g^{\prime}(x)$,
and for $x,y:[P]$ the image of $\operatorname{\textsf{{loop-comp}}}x\,y$ is
canonically induced by the fact that $g^{\prime}$ preserves group
multiplication.

Since $\operatorname{K}([P],1)$ is a groupoid, in order to show that
$f(g(x))=x$ for every $x:\operatorname{K}([P],1)$, it is enough to show that
it holds for $x:=\star$, which is the case by definition of $f$ and $g$, and
that this property is preserved under $\operatorname{\textsf{{loop}}}x$ for
$x:[P]$, which follows from the fact that we have
$f^{=}(g^{\prime}(x))=\operatorname{\textsf{{loop}}}x$ for any $x:[P]$ (this
is easily shown by induction on $x$). Conversely, we have to show that
$g(f(x))=x$ holds for $x:\operatorname{B}P$. Again, this is shown by induction
on $x$.

As an interesting remark, the careful reader will note that the fact that the
types $X$ and $R$ are sets does not play a role in the proof: in fact, those
assumptions can be dropped here. Also, note that we do not need the choice of
a representative in $X^{*}$ for every element of $[P]$ in order to define the
function $g$ from $\operatorname{\textsf{{gen}}}^{*}$ in the above proof:
intuitively, this is because the induced function $g$ does not depend on such
a choice of representatives. Finally, we should mention here that a similar
result is mentioned as an exercise in [27, Example 8.7.17]; the proof
suggested there is more involved since it is based on a generalized van Kampen
theorem.

######  Example 3.5.

The dihedral group $D_{5}$, see Example 5.6, admits the presentation

$\langle r,s\ |\
r^{4}=srs,sr^{2}s=r^{3},rsr=s,r^{3}s=sr^{2},sr^{3}=r^{2}s,s^{2}=1\rangle$

Hence, by Theorem 3.3 we can construct a delooping of $D_{5}$ as an higher
inductive type generated by two loops (corresponding to $r$ and $s$) and six
$2$-dimensional cells (corresponding to the relations). Note that this is much
smaller than $\operatorname{K}(D_{5},1)$ (it has 2 instead of 10 generating
loops, and 6 instead of 100 relations), thus resulting in shorter proofs when
reasoning by induction.

######  Example 3.6.

Any group $G$ admits a presentation, the _standard presentation_ , with one
generator $\underline{a}$ for every element $a:G$, and relations
$\underline{a}\,\,\underline{b}=\underline{ab}$ for every pair of generators,
as well as $\underline{1}=1$. By applying Theorem 3.3, we actually recover the
inductive type $\operatorname{K}(G,1)$ as delooping of $G$.

##  4 Delooping with torsors

In this section, we recall the other classical approach to constructing
deloopings of groups by using $G$-torsors, which originates in classical
constructions of algebraic topology [12]. Most of the material of the section
is already known, for which reason proofs are not much detailed. A more in-
depth presentation can be found in recent works such as [2, 5].

### Group actions

Given a group $G$ and a set $A$, an _action_ of $G$ on $A$ is a group morphism
from $G$ to $A\simeq A$, that is a map $\alpha:G\to(A\simeq A)$ such that

$\displaystyle\alpha(xy)$ $\displaystyle=\alpha(x)\circ\alpha(y)$
$\displaystyle\alpha(1)$ $\displaystyle=\operatorname{id}_{A}$ (2)

for all $x,y:G$.

A _$G$ -set_ is a set equipped with an action of $G$, and we write
$\operatorname{Set}_{G}$ for the type of $G$-sets. We often simply denote a
$G$-set by the associated action $\alpha$ and write
$\operatorname{dom}(\alpha)$ for the set on which $G$ acts.

######  Lemma 4.1 (GSetProperties.isGroupoidGSet).

The type $\operatorname{Set}_{G}$ is a groupoid.

######  Proof 4.2.

The type of sets is a groupoid [27, Theorem 7.1.11]. Given a set $A$, the type
of functions $A\to A$ is a set [27, Theorem 7.1.9] and thus a groupoid.
Finally, the axioms Equation 2 of actions are propositions (because $A$ is a
set) and thus groupoids. We conclude since groupoids are closed under
$\Sigma$-types [27, Theorem 7.1.8].

Given $G$-sets $\alpha$ and $\beta$, a _morphism_ between them consists of a
function $f:\operatorname{dom}{\alpha}\to\operatorname{dom}{\beta}$ which
preserves the group action, in the sense that for every $x:G$ and
$a:\operatorname{dom}{\alpha}$, we have

$\beta(x)(f(a))=f(\alpha(x)(a))\text{.}$ (3)

A morphism which is also an equivalence is called an _isomorphism_ and we
write $\alpha\simeq^{\operatorname{Set}_{G}}\beta$ for the type of
isomorphisms between $\alpha$ and $\beta$. We write
$\operatorname{Aut}(\alpha)$ for the type of automorphisms
$\alpha\simeq^{\operatorname{Set}_{G}}\alpha$, which is a group under
composition. The equalities between $G$-sets can be conveniently characterized
as follows.

######  Proposition 4.3 (GSetProperties.GSet≡Decomp).

Given two $G$-sets $\alpha$ and $\beta$, an equality between them consists of
an equality $p:\operatorname{dom}{\alpha}=\operatorname{dom}{\beta}$ such that
the function induced by transport along $p$, namely
$p^{\to}:\operatorname{dom}\alpha\to\operatorname{dom}\beta$, is a morphism of
$G$-sets.

######  Proof 4.4.

The characterization of equalities between $\Sigma$-types [27, Theorem 2.7.2]
entails that an equality between $(\operatorname{dom}{\alpha},\alpha)$ and
$(\operatorname{dom}{\beta},\beta)$ is a pair consisting of an equality
$p:\operatorname{dom}{\alpha}=\operatorname{dom}{\beta}$ and an equality
$q:p^{\to}(\alpha)=\beta$ (we can forget about the equality between the
components expressing the properties required for group actions since those
are propositions). By [27, Lemma 2.9.6] and function extensionality, we
finally have that the type of $q$ is equivalent to the type $\beta(x)\circ
p^{\to}=p^{\to}\circ\alpha(x)$.

It easily follows from this proposition that any equality between $G$-sets
induces an isomorphism of $G$-sets, as customary for equalities between
algebraic structures [27, Section 2.14]. In fact, this map from equalities to
isomorphisms can itself be shown to be an equivalence:

######  Proposition 4.5 (GSetProperties.GSetPath).

Given $G$-sets $\alpha$ and $\beta$, the canonical function

$(\alpha=\beta)\to(\alpha\simeq^{\operatorname{Set}_{G}}\beta)$

is an equivalence. Moreover, given a $G$-set $\alpha$, the induced equivalence

$(\alpha=\alpha)\simeq(\alpha\simeq^{\operatorname{Set}_{G}}\alpha)$

is compatible with the canonical group structures on both types.

######  Proof 4.6.

This is actually an instance of a more general correspondence between
equalities and isomorphisms of algebraic structures, which is known under the
name of _structure identity principle_ , see [11] and [27, Section 9.8], and
can be understood as a generalisation of univalence for types having an
algebraic structure.

### Torsors

For any group $G$, there is a canonical $G$-set called the _principal
$G$-torsor_ and noted $\operatorname{P}_{G}$, corresponding to the action of
$G$ on itself by left multiplication. Moreover, its group of automorphisms is
precisely the group $G$:

######  Proposition 4.7 (Deloopings.PGloops).

Given a group $G$, we have an equality of groups

$(\operatorname{P}_{G}\simeq^{\operatorname{Set}_{G}}\operatorname{P}_{G})=G$

######  Proof 4.8.

The two functions $\phi:\operatorname{Aut}\operatorname{P}_{G}\to G$ and
$\psi:G\to\operatorname{Aut}\operatorname{P}_{G}$, respectively defined by
$\phi(f):=f(1)$ and $\psi(x)(y):=yx$ are mutually inverse group morphisms, see
Appendix A.

The type $\operatorname{Set}_{G}$ is thus “almost” a delooping of $G$. Namely,
it is a groupoid (Lemma 4.1), which is pointed by $\operatorname{P}_{G}$ and
satisfies $\operatorname{\Omega}\operatorname{Set}_{G}=G$ by Propositions 4.5
and 4.7. It only lacks being connected, which can easily be addressed. Given a
pointed type $A$, its _connected component_ $\operatorname{Comp}A$ is the type
$\Sigma(x:A).\|\star=x\|_{-1}$. It is well-known that this type is pointed by
$(\star,|\operatorname{refl}|_{-1})$, connected and has the same loop space as
the original type, i.e. we have
$\operatorname{\Omega}\operatorname{Comp}A=\operatorname{\Omega}A$, see
Appendix C. We thus have:

######  Theorem 4.9 (Deloopings.torsorDeloops).

The connected component of $\operatorname{P}_{G}$ in $\operatorname{Set}_{G}$,
i.e. the type
$\operatorname{Comp}(\operatorname{Set}_{G},\operatorname{P}_{G})$, is a
delooping of $G$.

The elements of the connected component of the principal $G$-set are usually
called _$G$ -torsors_.

##  5 Generated torsors

Fix a group $G$. Given a set $X$ and a map $\gamma:X\to G$, we say that $X$
_generates_ $G$ (with respect to $\gamma$) when $\gamma^{*}:X^{*}\to G$ is
surjective. From now on, we suppose that we are in such a situation. We now
provide a variant for the construction of a delooping of $G$ by $G$-torsors
described in the previous section, taking advantage of the additional data of
a generating set in order to obtain smaller and simpler constructions. Note
that here, contrarily to Section 3, we only need a set of generators, not a
full presentation.

### Actions of sets

Given a type $A$, we write $\operatorname{End}A$ for its type of
_endomorphisms_ , i.e. maps $A\to A$. An _action_ of the set $X$ on a set $A$
is a morphism $X\to\operatorname{End}A$, i.e. a family of endomorphisms of $A$
indexed by $X$. We write $\operatorname{Set}_{X}$ for the type

$\operatorname{Set}_{X}\quad:=\quad\Sigma(A:\operatorname{Set}).(X\to\operatorname{End}A)$

of actions of $X$. An element $\alpha$ of this type consists in a set
$\operatorname{dom}\alpha$ with a function
$\alpha:X\to\operatorname{End}(\operatorname{dom}\alpha)$ and is called an
_$X$ -set_. A _morphism_ between $X$-sets $\alpha$ and $\beta$ is a function
$f:\operatorname{dom}\alpha\to\operatorname{dom}\beta$ satisfying Equation 3
for every $x:X$. The identities between $X$-sets can be characterized in a
similar way as for $G$-sets, see Proposition 4.3, and Proposition 4.5 also
extends in the expected way.

Precomposition by $\gamma$ induces a function
$U:\operatorname{Set}_{G}\to\operatorname{Set}_{X}$ which can be thought of as
a forgetful functor from $G$-sets to $X$-sets. Note that $U$ depends on
$\gamma$ but we leave it implicit for concision.

### Applications of the generated delooping

We have seen in the previous section that the connected component of the
principal $G$-torsor $P_{G}$ in $G$-sets is a delooping of $G$. Our aim in
this section is to show here that this construction can be simplified by
taking the connected component of the restriction of $P_{G}$ to $X$-sets.

Before proving this theorem, which is formally stated as Theorem 5.3 below, we
shall first illustrate its use on a concrete example. Consider
$\mathbb{Z}_{n}$, the cyclic group with $n$ elements. We write
$s:\mathbb{Z}_{n}\to\mathbb{Z}_{n}$ for the successor (modulo $n$) function,
which is an isomorphism. By Theorem 4.9, we know that the type

$\Sigma(A:\operatorname{Set}_{\mathbb{Z}_{n}}).\|\operatorname{P}_{\mathbb{Z}_{n}}=A\|_{-1}$

of $\mathbb{Z}_{n}$-torsors is a model of $\operatorname{B}\mathbb{Z}_{n}$.
This type is the connected component of the principal $\mathbb{Z}_{n}$-torsor
$\operatorname{P}_{\mathbb{Z}_{n}}$ in the universe
$\operatorname{Set}_{\mathbb{Z}_{n}}$ of sets with an action of
$\mathbb{Z}_{n}$, i.e. sets $A$ equipped with a morphism
$\alpha:\mathbb{Z}_{n}\to\operatorname{Aut}A$. Such a set $A$ is thus comes
with one automorphism $\alpha(k)$ for every element $k:\mathbb{Z}_{n}$,
therefore $k$ automorphisms in this case. However, most of them are
superfluous: $1$ generates all the elements of $\mathbb{Z}_{n}$ by addition,
so $\alpha(1)$ generates all the $\alpha(k)$ by composition because
$\alpha(k)=\alpha(1)^{k}$. The useful data of a $\mathbb{Z}_{n}$-set thus
boils down to a set $A$ together with one automorphism
$\alpha:\operatorname{Aut}A$ such that $\alpha^{n}=\operatorname{id}_{A}$.

Indeed, writing
$\operatorname{Set}^{\circlearrowleft}:=\Sigma(A:\operatorname{Set}).\operatorname{End}A$
for the type of all _endomorphisms_ (on any set), our theorem will imply that
the type

$\Sigma((A,f):\operatorname{Set}^{\circlearrowleft}).\|(\mathbb{Z}_{n},s)=(A,f)\|_{-1}$
(4)

(the connected component of the successor modulo $n$ in the universe of set
endomorphisms) is still a delooping of $\mathbb{Z}_{n}$. Note that we didn’t
assume that $f$ is an isomorphism nor that it should verify
$f^{n}=\operatorname{id}$. This is because both properties follow from the
fact that $f$ is in the connected component of the successor (which satisfies
those properties). Similarly, we do not need to explicitly assume that the
domain of the endomorphism is a set.

Our theorem thus allows to define, in a relatively simple way, types
corresponding to deloopings of groups. As recalled in the introduction, this
is particularly useful when one is not disposed to use higher inductive types
(e.g. because their definition, implementation and semantics are not entirely
mature). This is in fact the reason why this approach was used in UnitMath to
define the circle [3], and we provide a generic way to similarly define other
types. We expect that it can be used to reason about groups and compute
invariants such as their cohomology [8, 6, 4]. On a side note, one might be
worried by the fact that we are “biased” (by using a particular set of
generators), which allows us to be more concise but might make more difficult
generic proofs compared to $G$-torsors: we expect that this is not the case
because in order to define the group $G$ itself, one usually needs to resort
to a presentation, and thus is also biased in some sense…

### The generated delooping

In the following, we write $\operatorname{P}_{X}$ for $U\operatorname{P}_{G}$.

######  Proposition 5.1 (XSetProperties.theorem).

We have a group equivalence
$\operatorname{\Omega}\operatorname{P}_{G}\simeq\operatorname{\Omega}\operatorname{P}_{X}$.

######  Proof 5.2.

From Proposition 4.3, an element of $\operatorname{\Omega}P_{G}$ consists of
an equality $p:G=G$ in $\mathcal{U}$ such that

$\operatorname{P}_{G}(x)\circ p^{\to}=p^{\to}\circ\operatorname{P}_{G}(x)$

for every $x:G$. By function extensionality and the definition of the action
$\operatorname{P}_{G}$, this is equivalent to requiring, for every $g,z:G$
that

$g(p^{\to}(z))=p^{\to}(gz)$ (5)

Note that the above equality is between elements of $G$, which is a set, and
is thus a proposition. Similarly, an element of
$\operatorname{\Omega}\operatorname{P}_{X}$ consists of an equality $p:G=G$ in
$\mathcal{U}$ satisfying

$\gamma(x)(p^{\to}(z))=p^{\to}(\gamma(x)z)$ (6)

for every $x:X$ and $z:G$.

Clearly, any equality $p:G=G$ in $\operatorname{\Omega}\operatorname{P}_{G}$
also belongs to $\operatorname{\Omega}\operatorname{P}_{X}$ since the
condition Equation 6 is a particular case of Equation 5. We thus have a
function
$\phi:\operatorname{\Omega}\operatorname{P}_{G}\to\operatorname{\Omega}\operatorname{P}_{X}$.
Conversely, consider an element $p:G=G$ of
$\operatorname{\Omega}\operatorname{P}_{X}$, i.e. satisfying Equation 6 for
every $x:X$ and $z:G$. Our aim is to show that it belongs to
$\operatorname{\Omega}\operatorname{P}_{G}$. Given $g,z:G$, we thus want to
show that Equation 5 holds. Since $\gamma^{*}$ is surjective, because $X$
generates $G$, we know that there merely exists an element $u$ of $X^{*}$ such
that $\gamma^{*}(u)=x$. Since Equation 5 is a proposition, by the elimination
principle of propositional truncation, we can actually suppose given such a
$u$, and we have

$\displaystyle x(p^{\to}(y))$ $\displaystyle=\gamma^{*}(u)(p^{\to}(y))$ since
$\gamma^{*}(u)=x$ $\displaystyle=p^{\to}(\gamma^{*}(u)y)$ by repeated
application of Equation 6 $\displaystyle=p^{\to}(xy)$ since $\gamma^{*}(u)=x$.

The second equality essentially corresponds to the commutation of the
following diagram, where $u:=x_{1}x_{2}\ldots x_{n}$ with $x_{i}:X$:

${G}$${G}$${G}$${\ldots}$${G}$${G}$${G}$${G}$${G}$${\ldots}$${G}$${G}$$\scriptstyle{p^{\to}}$$\scriptstyle{\gamma(x_{1})}$$\scriptstyle{p^{\to}}$$\scriptstyle{\gamma(x_{2})}$$\scriptstyle{p^{\to}}$$\scriptstyle{p^{\to}}$$\scriptstyle{\gamma(x_{n})}$$\scriptstyle{p^{\to}}$$\scriptstyle{\gamma(x_{1})}$$\scriptstyle{\gamma(x_{2})}$$\scriptstyle{\gamma(x_{n})}$

This thus induces a function
$\psi:\operatorname{\Omega}\operatorname{P}_{X}\to\operatorname{\Omega}\operatorname{P}_{G}$.
The functions $\phi$ and $\psi$ clearly preserve the group structure (given by
concatenation of paths) and are mutually inverse of each other, hence we have
the equivalence we wanted.

######  Theorem 5.3.

The type $\operatorname{Comp}\operatorname{P}_{X}$ is a delooping of $G$.

######  Proof 5.4.

Since taking the connected component preserves loops spaces (Proposition C.5),
we have that $\operatorname{\Omega}\operatorname{Comp}\operatorname{P}_{X}$ is
equal to $\operatorname{\Omega}\operatorname{P}_{X}$, which in turn is equal
to $\operatorname{\Omega}\operatorname{P}_{G}$ by Proposition 5.1, and thus to
$G$ by Theorem 4.9.

The delooping of $G$ constructed in previous theorem is the component of
$\operatorname{P}_{X}$ in $X$-sets:

$\Sigma(A:\mathcal{U}).\Sigma(S:\operatorname{isSet}A).\Sigma(f:X\to\operatorname{End}A).\|\operatorname{P}_{X}=(A,S,f)\|_{-1}$

Since for any type $A$, the type $\operatorname{isSet}A$ is a proposition [27,
Theorem 7.1.10], and the underlying type of $\operatorname{P}_{X}$ is a set,
the underlying type of any $X$-set in the connected component of
$\operatorname{P}_{X}$ will also be a set. As a consequence, the above type
can slightly be simplified, by dropping the requirement that $A$ should be a
set:

######  Proposition 5.5.

The type
$\Sigma(A:\mathcal{U}).\Sigma(f:X\to\operatorname{End}A).\|\operatorname{P}_{X}=(A,f)\|_{-1}$
is a delooping of $G$.

For instance, the delooping Equation 4 of $\mathbb{Z}_{n}$ can slightly be
simplified as

$\Sigma((A,f):\mathcal{U}^{\circlearrowleft}).\|(\mathbb{Z}_{n},s)=(A,f)\|_{-1}$

where
$\mathcal{U}^{\circlearrowleft}:=\Sigma(A:\mathcal{U}).\operatorname{End}A$ is
the type of all endomorphisms of the universe.

######  Example 5.6.

Theorem 5.3 applies to every group for which a generating set is known (and,
of course, the smaller the better). For instance, given a natural number $n$,
the _dihedral group_ $D_{n}$ is the group of symmetries of a regular polygon
with $n$ sides. It has $2n$ elements and is generated by two elements $s$
(axial symmetry) and $r$ (rotation by an angle of $2\pi/n$). Hence the
connected component of the symmetry and the rotation in the type of pairs of
set endomorphisms, i.e.

$\Sigma(A:\operatorname{Set}).\Sigma(f,g:\operatorname{End}A\times\operatorname{End}A).\|(D_{n},s,r)=(A,f,g)\|_{-1}$

is a delooping of the dihedral group $D_{n}$.

### Alternative proof

We would like to provide another proof Proposition 5.1, which was suggested by
an anonymous reviewer. It is based on the idea that in order to show
$\operatorname{\Omega}\operatorname{P}_{X}\simeq\operatorname{\Omega}\operatorname{P}_{G}$,
it is enough to show that $U:\operatorname{Set}_{G}\to\operatorname{Set}_{X}$
is an _embedding_ , i.e. that for every $\alpha,\beta:\operatorname{Set}_{G}$
the induced function $U^{=}:(\alpha=\beta)\to(U\alpha=U\beta)$ between path
spaces is an equivalence [27, Definition 4.6.1]. It relies on the following
result whose proof can be found in Appendix A.

######  Lemma 5.7.

Given a type $A:\mathcal{U}$, type families $P,Q:A\to\mathcal{U}$ and
$f:(a:A)\to P\,a\to Q\,a$, the map $\Sigma A.f:\Sigma A.P\to\Sigma A.Q$ is an
embedding if and only if $f\,a:P\,a\to Q\,a$ is an embedding for every $a:A$.

######  Proposition 5.8.

The map $U:\operatorname{Set}_{G}\to\operatorname{Set}_{X}$ is an embedding.

######  Proof 5.9.

Given a morphism of groups $f:H\to K$, we write
$\operatorname{Set}_{f}:\operatorname{Set}_{K}\to\operatorname{Set}_{H}$ for
the function induced by precomposition. In particular, by definition, we have
$U:=\operatorname{Set}_{\gamma}$. The function $\gamma:X\to G$ can be
decomposed as $\gamma^{*}\circ\iota$, and therefore
$\operatorname{Set}_{\gamma}$ can be decomposed as
$\operatorname{Set}_{\iota}\circ\operatorname{Set}_{\gamma^{*}}$:

${\operatorname{Set}_{X^{*}}}$${\operatorname{Set}_{G}}$${\operatorname{Set}_{X}}$$\scriptstyle{\operatorname{Set}_{\iota}}$$\scriptstyle{\operatorname{Set}_{\gamma^{*}}}$$\scriptstyle{U}$

Both maps are embeddings so that $U$ is an embedding by composition. Namely,

  * •

_$\operatorname{Set}_{\gamma^{*}}$ is an embedding_. Consider the map

$F:(A:\operatorname{Set})\to(G\to_{\operatorname{Grp}}\operatorname{Aut}A)\to(X^{*}\to_{\operatorname{Grp}}\operatorname{Aut}A)$

obtained by precomposition by $\gamma^{*}$. Since $\gamma^{*}$ is surjective
we have that $F\,A$ is an embedding for every set $A$ [27, Lemma 10.1.4]. By
Lemma 5.7, we deduce that $\Sigma\operatorname{Set}.F$, which is
$\operatorname{Set}_{\gamma^{*}}$, is an embedding.

  * •

_$\operatorname{Set}_{\iota}$ is an embedding_. By universal property of
$X^{*}$, given a set $A$, the map

$(X^{*}\to_{\operatorname{Grp}}\operatorname{Aut}A)\to(X\to\operatorname{Aut}A)$

obtained by precomposition by $\iota$ is an equivalence, and thus an
embedding. Moreover, the property of being an isomorphism is a proposition,
hence the forgetful map

$(X\to\operatorname{Aut}A)\to(X\to\operatorname{End}A)$

is an embedding because its fibers are propositions. Since embeddings are
stable under composition, we deduce that the induced map

$F:(A:\operatorname{Set})\to(X^{*}\to_{\operatorname{Grp}}\operatorname{Aut}A)\to(X\to\operatorname{End}A)$

is such that $F\,A$ is an embedding for every set $A$. By Lemma 5.7, the map
$\Sigma\operatorname{Set}.F$, which is $\operatorname{Set}_{\iota}$, is thus
an embedding.

##  6 Cayley graphs

We have seen in Section 3 that a delooping of $G$ can be obtained by further
homotopy quotienting a delooping of $X^{*}$. The kernel of the map
$\gamma^{*}:X^{*}\to G$ measures the defect of $X^{*}$ from being $G$, which
corresponds to the relations of the group. We show here that, under the
delooping operation, those relations are precisely encoded by the Cayley graph
[9, 19], a classical and useful construction in group theory which can be
associated to any generated group.

The _Cayley graph_ of $G$, with respect to the generating set $X$, is the
directed graph whose vertices are the elements of $G$, and such that for every
vertex $g:G$ and generator $x:X$, we have an edge $g\to gx$. In homotopy type
theory, it is thus natural to represent it as the higher inductive type
$\operatorname{C}(X,G)$ defined as

$\begin{array}[]{l@{\ :\
}l}\operatorname{\textsf{{vertex}}}&G\to\operatorname{C}(X,G)\\\
\operatorname{\textsf{{edge}}}&(g:G)(x:X)\to\operatorname{\textsf{{vertex}}}g=\operatorname{\textsf{{vertex}}}(gx)\end{array}$

For instance, the Cayley graphs associated to $\mathbb{Z}_{5}$ (with $2$ as
generator) and $D_{5}$ (with $r$ and $s$ as generators) are respectively

$\scriptstyle 0$$\scriptstyle 1$$\scriptstyle 2$$\scriptstyle 3$$\scriptstyle
4$ $\scriptstyle r$$\scriptstyle r$$\scriptstyle s$$\scriptstyle
s$$\scriptstyle r$$\scriptstyle r$$\scriptstyle s$$\scriptstyle
s$$\scriptstyle r$$\scriptstyle r$$\scriptstyle s$$\scriptstyle
s$$\scriptstyle r$$\scriptstyle r$$\scriptstyle s$$\scriptstyle
s$$\scriptstyle r$$\scriptstyle r$$\scriptstyle s$$\scriptstyle s$

Our main result in this section is that this type satisfies the following
property. We recall that the delooping operation is functorial, see Appendix B
and [29]: in particular, we can deloop morphisms. We also recall that the
_kernel_ of a map $f:A\to B$ with $B$ pointed is its fiber at the
distinguished element $\star$ of $B$.

######  Theorem 6.1 (Cayley.Cayley-ker).

The type $\operatorname{C}(X,G)$ is the kernel of the function
$\operatorname{B}\gamma^{*}:\operatorname{B}X^{*}\to\operatorname{B}G$ induced
by $\gamma$, i.e. we have

$\operatorname{C}(X,G)\quad=\quad\Sigma(x:\operatorname{B}X^{*}).(\star=\operatorname{B}\gamma^{*}(x))\text{.}$

######  Proof 6.2.

We define the type family $P:\operatorname{B}X^{*}\to\mathcal{U}$ by
$P(x)=(\star=\operatorname{B}\gamma^{*}(x))$. Remember that
$\operatorname{B}X^{*}$ admits a description as a coequalizer, see Equation 1
and Proposition 3.1. Hence, by the flattening lemma for coequalizers (see
Lemma D.1 and [27, Section 6.12]), we have a coequalizer of total spaces

${\Sigma X.P(\star)}$${\Sigma
1.P(\star)}$${\Sigma\operatorname{B}X^{*}.P}$$\scriptstyle{(x,p)\mapsto(\star,p)}$$\scriptstyle{(x,p)\mapsto(\star,P^{\to}_{p}(x))}$

By using the properties of transport in path spaces [27, Theorem 2.11.3], it
can be shown that the bottom map sends $(x,p)$ to
$(\star,p\cdot\operatorname{B}\gamma^{*}(x))$. Moreover,
$\operatorname{B}\gamma^{*}$ is pointed, so $P(\star)$ is equal to
$\operatorname{\Omega}\operatorname{B}G$, i.e. $G$, and we have the following
coequalizer:

${X\times G}$${G}$${\Sigma\operatorname{B}X^{*}.P}$$\scriptstyle{(x,g)\mapsto
g}$$\scriptstyle{(x,g)\mapsto gx}$

If follows that $\Sigma\operatorname{B}X^{*}.P$ consists in $|G|$ points and a
path $g=gx$ for each pair $(x,g):X\times G$, and is therefore equal to the
Cayley graph $\operatorname{C}(X,G)$.

The above result can be interpreted as stating that we have a fiber sequence
(see [27, Section 8.4])

${\operatorname{C}(X,G)}$${\operatorname{B}X^{*}}$${\operatorname{B}G}$

which encodes the fact that we have an action of $G$ on its Cayley graph,
whose homotopy quotient $\operatorname{C}(X,G)\mathop{\\!/\\!\\!/\\!}G$ is
$\operatorname{B}X^{*}$, see [21, Proposition 16]. Hence, we recover the
canonical action of $G$ on its Cayley graph.

### Relations

The long exact sequence of homotopy groups induced by the above fiber sequence
[27, Theorem 8.4.6] implies in particular that we have the following short
exact sequence of groups

${0}$${\operatorname{\Omega}\operatorname{C}(X,G)}$${X^{*}}$${G}$${0}$

which shows that $\operatorname{\Omega}\operatorname{C}(X,G)$ is the (free)
group encoding relations of $G$ with respect to $X$. Indeed, we have that
$\operatorname{C}(X,G)=\operatorname{B}R^{*}$ where $R$ is a choice of
$|G|\times(|X|-1)+1$ relations: those are the loops in the Cayley graph after
contracting $|G|-1$ edges to obtain a wedge of circles. In some sense, Theorem
6.1 provides an internalization of the fact that $G$ is presented by $\langle
X\ |\ R\rangle$, contrasting with the point of view developed in Section 3.

### The Cayley complex and higher variants

We now briefly explain that we can extend the previous construction in higher
dimensions in order to define internally a type corresponding to the classical
_Cayley complex_ [19]. Suppose given a presentation $P:=\langle X\ |\
R\rangle$ for $G$ and write $\operatorname{B}_{2}P$ for the $2$-skeleton of
the type $\operatorname{B}P$ defined in Section 3 (i.e. the type generated by
$\star$, $\operatorname{\textsf{{gen}}}$, and $\operatorname{\textsf{{rel}}}$,
but without the truncation $\operatorname{\textsf{{trunc}}}$). As in previous
section, this type can be considered as an approximation of
$\operatorname{B}P$ (lacking the truncation) and we would like to measure the
difference between the two types. The _Cayley complex_ $\operatorname{C}P$
associated to the presentation $P$ is the inductive type defined by

$\begin{array}[]{l@{\ :\
}l}\operatorname{\textsf{{vertex}}}&G\to\operatorname{C}P\\\
\operatorname{\textsf{{edge}}}&(g:G)(x:X)\to\operatorname{\textsf{{vertex}}}g=\operatorname{\textsf{{vertex}}}(gx)\\\
\operatorname{\textsf{{cell}}}&(g:G)(r:R)\to(\operatorname{\textsf{{edge}}}g)^{*}(\pi(r))=(\operatorname{\textsf{{edge}}}g)^{*}(\pi^{\prime}(r))\end{array}$

where, given $g:G$ and $u:=x_{1}x_{2}\ldots x_{n}:X^{*}$, we have that
$(\operatorname{\textsf{{edge}}}g)^{*}\,u$ is the path

${\operatorname{\textsf{{v}}}g}$${\operatorname{\textsf{{v}}}(gx_{1})}$${\operatorname{\textsf{{v}}}(gx_{1}x_{2})}$${\cdots}$${\operatorname{\textsf{{v}}}(gx_{1}\ldots
x_{n-1})}$${\operatorname{\textsf{{v}}}(gx_{1}\ldots
x_{n})}$$\scriptstyle{\operatorname{\textsf{{e}}}g\,x_{1}}$$\scriptstyle{\operatorname{\textsf{{e}}}(gx_{1})\,x_{2}}$$\scriptstyle{\ldots}$$\scriptstyle{\ldots}$$\scriptstyle{\operatorname{\textsf{{e}}}g(x_{1}\ldots
x_{n-1})\,x_{n}}$

where $\operatorname{\textsf{{v}}}$ (resp. $\operatorname{\textsf{{e}}}$) is a
short notation for $\operatorname{\textsf{{vertex}}}$ (resp.
$\operatorname{\textsf{{edge}}}$). We will detail in future works the proof of
the following result, which can be performed using the flattening lemma for
pushouts, as in Theorem 6.1:

######  Theorem 6.3.

We have a fiber sequence
${\operatorname{C}P}$${\operatorname{B}_{2}P}$${\operatorname{B}G\text{.}}$

In fact, this resolution-like process can be iterated in order to obtain
better and better approximations $\operatorname{B}_{n}P$ of
$\operatorname{B}G$, and higher Cayley complexes as the fibers of the
canonical maps $\operatorname{B}_{n}P\to\operatorname{B}G$. Moreover, the join
construction [23, 24] provides a way to automate this task, see for instance
[7, 21].

##  7 Future works

We have presented two ways to improve in practice the known constructions of
deloopings of groups when we have a presentation of the group. This work is
part of a larger investigation of “efficient” models of groups deloopings, in
the sense that we can compute effectively with those. In particular, the
construction of the infinite real projective space performed by Buchholtz and
Rijke [7], provides a cellular description of $\operatorname{B}\mathbb{Z}_{2}$
(which is better than the usual ones obtained by generic methods because it
consists in a _non-recursive_ higher inductive type). In other current work,
we refine their approach in order to construct lens spaces and thus obtain a
cellular version of $\operatorname{B}\mathbb{Z}_{n}$ for every natural number
$n$, as well as efficient representations of deloopings of other classical
groups [21]. More generally, the formalization of group theory in univalent
foundations is still under heavy investigation [2], and we aim at developing
general techniques to construct efficient representations of (internal) groups
in homotopy type theory, which would open the way to cohomological
computations [8, 6, 4] or the definition of group actions on higher types (as
a generalization of group actions on sets). On another note, higher-inductive
types play a role in homotopy type theory analogous to the one of polygraphs
for strict higher categories: numerous techniques have been developed for
those [1], notably based on rewriting, and we plan to adapt them in this
setting, following first developments of [16].

## References

  * [1] Dimitri Ara, Albert Burroni, Yves Guiraud, Philippe Malbos, François Métayer, and Samuel Mimram.  Polygraphs: From rewriting to higher categories.  To appear, 2023.  arXiv:2312.00429.
  * [2] Marc Bezem, Ulrik Buchholtz, Pierre Cagne, Bjørn Ian Dundas, and Daniel R. Grayson.  Symmetry.  URL: https://github.com/UniMath/SymmetryBook.
  * [3] Marc Bezem, Ulrik Buchholtz, Daniel R Grayson, and Michael Shulman.  Construction of the circle in UniMath.  Journal of Pure and Applied Algebra, 225(10):106687, 2021.  arXiv:1910.01856, doi:10.1016/j.jpaa.2021.106687.
  * [4] Guillaume Brunerie, Axel Ljungström, and Anders Mörtberg.  Synthetic integral cohomology in cubical Agda.  In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2022.  doi:10.4230/LIPIcs.CSL.2022.11.
  * [5] Ulrik Buchholtz, J Daniel Christensen, Jarl G Taxerås Flaten, and Egbert Rijke.  Central H-spaces and banded types.  Preprint, 2023.  arXiv:2301.02636.
  * [6] Ulrik Buchholtz and Kuen-Bang Hou.  Cellular cohomology in homotopy type theory.  Logical Methods in Computer Science, 16, 2020.  arXiv:1802.02191, doi:10.23638/LMCS-16(2:7)2020.
  * [7] Ulrik Buchholtz and Egbert Rijke.  The real projective spaces in homotopy type theory.  In 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1–8. IEEE, 2017.  arXiv:1704.05770, doi:10.5555/3329995.3330081.
  * [8] Evan Cavallo.  Synthetic cohomology in homotopy type theory.  PhD thesis, MA thesis, 2015.
  * [9] Arthur Cayley.  Desiderata and suggestions. No. 2 – The theory of groups: graphical representation.  American journal of mathematics, 1(2):174–176, 1878.
  * [10] Camil Champin and Samuel Mimram.  Delooping generated groups.  URL: https://github.com/smimram/generated-deloopings-agda.
  * [11] Thierry Coquand and Nils Anders Danielsson.  Isomorphism is equality.  Indagationes Mathematicae, 24(4):1105–1120, 2013.  doi:10.1016/j.indag.2013.09.002.
  * [12] Michel Demazure and Pierre Gabriel.  Groupes Algébriques, Tome 1.  North-Holland Publishing Company, 1970.
  * [13] John RJ Groves.  Rewriting systems and homology of groups.  In Groups—Canberra 1989: Australian National University Group Theory Program 1989, pages 114–141. Springer, 2006.  doi:10.1007/BFb0100735.
  * [14] Krzysztof Kapulkin and Peter LeFanu Lumsdaine.  The simplicial model of Univalent Foundations (after Voevodsky).  Journal of the European Mathematical Society, 23(6):2071–2126, 2021\.  arXiv:1211.2851, doi:10.4171/jems/1050.
  * [15] Nicolai Kraus and Thorsten Altenkirch.  Free higher groups in homotopy type theory.  In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, pages 599–608, 2018.  arXiv:1805.02069, doi:10.1145/3209108.3209183.
  * [16] Nicolai Kraus and Jakob von Raumer.  A rewriting coherence theorem with applications in homotopy type theory.  Mathematical Structures in Computer Science, 32(7):982–1014, 2022\.  arXiv:2107.01594, doi:10.1017/S0960129523000026.
  * [17] Daniel R Licata and Eric Finster.  Eilenberg-MacLane spaces in homotopy type theory.  In Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1–9, 2014.  doi:10.1145/2603088.2603153.
  * [18] Peter LeFanu Lumsdaine and Michael Shulman.  Semantics of higher inductive types.  Mathematical Proceedings of the Cambridge Philosophical Society, 169(1):159–208, 2020.  arXiv:1705.07088, doi:10.1017/S030500411900015X.
  * [19] Roger C Lyndon and Paul E Schupp.  Combinatorial group theory, volume 188.  Springer, 1977.
  * [20] Per Martin-Löf.  Intuitionistic type theory, volume 1 of Studies in proof theory.  Bibliopolis, 1984.
  * [21] Émile Oleon and Samuel Mimram.  Delooping cyclic groups with lens spaces in homotopy type theory.  Accepted at LICS 2024 conference, 2024.
  * [22] Henri Poincaré.  Analysis situs.  Gauthier-Villars Paris, France, 1895.
  * [23] Egbert Rijke.  The join construction.  Preprint, 2017.  arXiv:1701.07538.
  * [24] Egbert Rijke.  Classifying Types.  PhD thesis, Carnegie Mellon University, July 2018.  arXiv:1906.09435.
  * [25] Egbert Rijke.  Introduction to homotopy type theory.  Preprint, 2022.  arXiv:2212.11082.
  * [26] The Agda Community.  Cubical Agda Library, July 2023.  URL: https://github.com/agda/cubical.
  * [27] The Univalent Foundations Program.  Homotopy Type Theory: Univalent Foundations of Mathematics.  Institute for Advanced Study, 2013.  URL: https://homotopytypetheory.org/book/.
  * [28] Andrea Vezzosi, Anders Mörtberg, and Andreas Abel.  Cubical Agda: A dependently typed programming language with univalence and higher inductive types.  Journal of Functional Programming, 31, 2021.  doi:10.1145/3341691.
  * [29] David Wärn.  Eilenberg–maclane spaces and stabilisation in homotopy type theory.  Journal of Homotopy and Related Structures, 18(2):357–368, 2023\.  arXiv:2301.03685, doi:10.1007/s40062-023-00330-5.
  * [30] David Wärn.  Path spaces of pushouts.  Preprint, 2023.  arXiv:2402.12339.

##  Appendix A Omitted proofs

######  Proof A.1 (Proof of Proposition 4.7).

The two functions

$\displaystyle\phi:\operatorname{Aut}\operatorname{P}_{G}$ $\displaystyle\to
G$ $\displaystyle\psi:G$
$\displaystyle\to\operatorname{Aut}\operatorname{P}_{G}$ $\displaystyle f$
$\displaystyle\mapsto f(1)$ $\displaystyle x$ $\displaystyle\mapsto y\mapsto
yx$

are group morphisms. Namely, given
$f,g:\operatorname{Aut}\operatorname{P}_{G}$, we have

$\displaystyle\phi(g\circ f)$ $\displaystyle=g\circ
f(1)=g(f(1)1)=f(1)g(1)=\phi(f)\phi(g)$ $\displaystyle\phi(\operatorname{id})$
$\displaystyle=\operatorname{id}(1)=1$

and given $x,y:G$, we have for every $z:G$,

$\displaystyle\psi(xy)(z)$ $\displaystyle=z(xy)=(zx)y=\psi(y)\circ\psi(x)(z)$
$\displaystyle\psi(1)(x)$ $\displaystyle=x1=\operatorname{id}(x)$

Moreover, they are mutually inverse. Namely, given
$f:\operatorname{Aut}\operatorname{P}_{G}$ and $x:G$, we have

$\displaystyle\psi\circ\phi(f)(x)$ $\displaystyle=xf(1)=f(x1)=f(x)$
$\displaystyle\phi\circ\psi(x)$ $\displaystyle=1x=x$

We thus have $\operatorname{Aut}\operatorname{P}_{G}\simeq G$ and we conclude
by univalence.

######  Proof A.2 (Proof of Lemma 5.7).

By definition, the map $\Sigma A.f$ is an embedding iff for every $(a,x)$ and
$(a^{\prime},x^{\prime})$ in $\Sigma AX$, the induced map

$(a,x)=(a^{\prime},x^{\prime})\to(a,f\,a\,x)=(a^{\prime},f\,a^{\prime}\,x^{\prime})$

is an equivalence. By the characterization of equalities in $\Sigma$-types
[27, Theorem 2.7.2], this map corresponds to a map

$(\Sigma(p:a=a^{\prime}).P^{\to}_{p}(x)=x^{\prime})\to(\Sigma(p:a=a^{\prime}).Q^{\to}_{p}(f\,a\,x)=f\,a^{\prime}\,x^{\prime})$

By [27, Theorem 4.7.7], this is an equivalence if and only if the fiber map

$(P^{\to}_{p}(x)=x^{\prime})\to(Q^{\to}_{p}(f\,a\,x)=f\,a^{\prime}\,x^{\prime})$

is an equivalence for every $p:a=a^{\prime}$. By path induction, this is true
if and only if

$(f\,a)^{=}:x=x^{\prime}\to f\,a\,x=f\,a\,x^{\prime}$

is an equivalence for all $a:A$, and $x,x^{\prime}:Xa$. By definition, this is
the requirement that $f\,a$ is an embedding for all $a:A$.

##  Appendix B Equivalence between internal and external groups

### Functoriality of delooping

One of the main properties of the delooping operation is that it is a “local
inverse” to taking loop spaces in the following sense:

######  Proposition B.1.

Given pointed connected groupoids $A$ and $B$ and a group morphism
$f:\operatorname{\Omega}A\to\operatorname{\Omega}B$, there is a unique pointed
morphism $g:A\to B$ such that $\operatorname{\Omega}g=f$.

######  Proof B.2.

By [29, Corollary 12], with $n=0$, we have that the type $\Sigma(g:A\to
B).\operatorname{\Omega}g=f$ is equivalent to $(p,q:\star_{A}=\star_{A})\to
f(p\cdot q)=f(p)\cdot f(q)$. This type is a proposition because
$\operatorname{\Omega}B$ is a set (because $B$ is a groupoid), and inhabited
(because $f$ is a morphism of groups), and thus contractible.

As an immediate consequence of the above lemma, deloopings are unique:

######  Proposition B.3.

Given two deloopings $\operatorname{B}G$ and $\operatorname{B}^{\prime}G$ of a
group $G$, we have $\operatorname{B}G=\operatorname{B}^{\prime}G$.

Given a group morphism $f:G\to H$ such that both $G$ and $H$ admit deloopings
(and this actually always holds by Theorem 4.9), the _delooping_ of $f$ is the
morphism

$\operatorname{B}f:\operatorname{B}G\to\operatorname{B}H$

associated, by Proposition B.1, to the morphism
$\operatorname{d}_{H}^{\leftarrow}\circ
f\circ\operatorname{d}_{G}^{\to}:\operatorname{\Omega}\operatorname{B}G\to\operatorname{\Omega}\operatorname{B}H$.
By Proposition B.1, this operation is functorial in the sense that that it
preserves identities and composition.

### Equivalence between the two points of view

Although this is not central in this article, we shall mention here the
fundamental equivalence provided by the above constructions; details can be
found in [2]. We write $\operatorname{IntGroup}$ for the type of internal
groups, i.e. pointed connected groupoids.

######  Theorem B.4.

The maps
$\operatorname{\Omega}:\operatorname{IntGroup}\to\operatorname{Group}$ and
$\operatorname{B}:\operatorname{Group}\to\operatorname{IntGroup}$ form an
equivalence of types.

######  Proof B.5.

Given a group $G$, we have $\operatorname{\Omega}\operatorname{B}G=G$ by
definition of $\operatorname{B}G$. Given an internal group $A$, we have
$\operatorname{B}\operatorname{\Omega}A\simeq A$ by Proposition B.3.

The above theorem thus states looping and delooping operators allow us to go
back and forth between the external and the internal point of view of group
theory in homotopy type theory. Note that the torsor construction only gives a
delooping in a larger universe than the original group unless one makes
additional assumptions such as the _replacement axiom_ [25, Axiom 18.1.8].

### Internal group actions

In a similar way that the traditional notion of group admits an internal
reformulation (Section 2), the notion of action also admits an internal
counterpart which can be defined as follows. Given a group $G$, an _internal_
action of $G$ on a set $A$ is a function

$\alpha:\operatorname{B}G\to\operatorname{Set}$

such that $\alpha(\star)=A$. Since $\operatorname{Set}$ is a groupoid [27,
Theorem 7.1.11], by Theorem B.4, we have equivalences of types

$(\operatorname{B}G\to\operatorname{Set})\quad\simeq\quad(\operatorname{\Omega}\operatorname{B}G\to\operatorname{\Omega}(\operatorname{Set},A))\quad\simeq\quad(G\to\operatorname{Aut}A)$

which show that internal group actions correspond to external ones: the
delooping operator internalizes an external group action, and the looping
operator externalizes an internal group action.

##  Appendix C Connected components

We define the _connected component_ of the pointed type $A$ as the type of
points which are merely connected to the distinguished point of $A$. This type
is noted $\operatorname{Comp}A$ (or $\operatorname{Comp}(A,\star)$ when we
want to specify the distinguished element $\star$). Formally,

$\operatorname{Comp}A\quad:=\quad\Sigma(x:A).\|\star=x\|_{-1}$

This type is canonically pointed by $(\star,|\operatorname{refl}|_{-1})$. This
construction deserves its name because it produces a connected space, whose
geometry is the same as the original space around the distinguished point, as
shown in the following two lemmas.

######  Lemma C.1 (Comp.isConnectedComp).

The type $\operatorname{Comp}A$ is connected.

######  Proof C.2.

It can be shown that a type $X$ is connected precisely when both $\|X\|_{-1}$
and $(x,y:X)\to\|x=y\|_{-1}$ are inhabited, i.e. when $X$ merely has a point
and any two points are merely equal [27, Exercise 7.6]. In our case, the type
$\operatorname{Comp}A$ is pointed and thus $\|\operatorname{Comp}A\|_{-1}$
holds. Moreover, suppose that there are two points $(x,p)$ and $(y,q)$ in
$\operatorname{Comp}A$ with $x,y:A$, $p:\|\star=x\|_{-1}$ and
$q:\|\star=y\|_{-1}$. Our goal is to show that $\|(x,p)=(y,q)\|_{-1}$ holds,
which is a proposition, so by elimination of propositional truncation, we can
therefore assume that $p$ (resp. $q$) has type $\star=x$ (resp. $\star=y$).
Hence, we can construct a path $p^{-}\cdot q$ of type $x=y$, and therefore
$(x,p)=(y,q)$ because the second components belong to a proposition by
propositional truncation. We conclude that $\|(x,p)=(y,q)\|_{-1}$ and finally
that $\operatorname{Comp}A$ is connected.

######  Lemma C.3 (Comp.loopCompIsLoop).

We have $\operatorname{\Omega}\operatorname{Comp}A=\operatorname{\Omega}A$.

######  Proof C.4.

We begin by showing that the type

$\Sigma((x,t):\operatorname{Comp}A).(\star=x)$ (7)

is contractible. In order to do so, observe that we have the following
equivalence of types:

$\displaystyle\Sigma((x,t):\operatorname{Comp}A).(\star=x)$
$\displaystyle\simeq\Sigma((x,t):\Sigma(x:A).\|\star=x\|_{-1}).(\star=x)$
$\displaystyle\simeq\Sigma(x:A).(\|\star=x\|_{-1})\times(\star=x)$
$\displaystyle\simeq\Sigma((x,p):\Sigma(x:A).(\star=x)).\|\star=x\|_{-1}$

using classical associativity and commutativity properties of $\Sigma$-types.
Moreover, the type $\Sigma(x:A).(\star=x)$ is contractible [27, Lemma 3.11.8],
therefore the whole type on the last line is a proposition (as a sum of
propositions over a proposition), and therefore also the original type
Equation 7. We write $\star^{\prime}$ for the element
$(\star,\|\operatorname{refl}_{\star}\|_{-1})$ of $\operatorname{Comp}A$. The
type Equation 7 is pointed by the canonical element
$(\star^{\prime},\operatorname{refl})$ and thus contractible as a pointed
proposition.

We have a morphism

$\begin{array}[]{r@{\ }c@{\ }c@{\ }c@{\ }c@{\
}l}F:&((x,t):\operatorname{Comp}A)&\to&(\star^{\prime}=(x,t))&\to&(\star=x)\\\
&(x,t)&&p&\mapsto&\pi^{=}(p)\end{array}$

sending a path $p$ to the path obtained by applying the first projection. It
canonically induces a morphism

$\displaystyle\Sigma((x,t):\operatorname{Comp}A).(\star^{\prime}=(x,t))$
$\displaystyle\to\Sigma((x,t):\operatorname{Comp}A).(\star=x)$
$\displaystyle((x,t),p)$ $\displaystyle\mapsto((x,t),\pi^{=}(p))$

between the corresponding total spaces. Since the left member is contractible
(by [27, Lemma 3.11.8] again) and the right member is contractible (as shown
above), this is an equivalence. By [27, Theorem 4.7.7], for every
$x:\operatorname{Comp}A$, the fiber morphism $Fx$ is also an equivalence. In
particular, with $x$ being $\star^{\prime}$, we obtain
$\operatorname{\Omega}\operatorname{Comp}A\simeq\operatorname{\Omega}A$ (as a
type) and we can conclude by univalence. Note that the equivalence preserves
the group structure so that the equality also holds in groups.

As a direct corollary of the two above lemmas, we have:

######  Proposition C.5.

Given a pointed groupoid $A$, $\operatorname{Comp}A$ is a delooping of
$\operatorname{\Omega}A$.

######  Remark C.6.

Some people write $\operatorname{Aut}A$ for $\operatorname{\Omega}A$ and the
above proposition states that we have
$\operatorname{B}\operatorname{Aut}A=\operatorname{Comp}A$. For this reason,
the (confusing) notation $\operatorname{BAut}A$ is also found in the
literature for $\operatorname{Comp}A$.

##  Appendix D The flattening lemma

We recall here the classical flattening lemma, see [27, Section 6.12] for a
more detailed presentation and proof.

######  Lemma D.1 (Flattening for coequalizers).

Suppose given a coequalizer

${A}$${B}$${C}$$\scriptstyle{f}$$\scriptstyle{g}$$\scriptstyle{h}$

with $p:h\circ f=h\circ g$, and a type family $P:C\to\mathcal{U}$. Then the
diagram

${\Sigma A.(P\circ h\circ f)}$${\Sigma B.(P\circ h)}$${\Sigma
C.P}$$\scriptstyle{\Sigma
f.(\lambda\\_.\operatorname{id}{})}$$\scriptstyle{\Sigma
g.e}$$\scriptstyle{\Sigma h.(\lambda\\_.\operatorname{id}{})}$

is a coequalizer, where the map

$e:(a:A)\to P(h(f(a)))\to P(h(g(a)))$

is induced by transport along $p$ by

$e\,a\,x:=P^{\to}_{p(a)}(x)\text{.}$

Note that there is a slight asymmetry: we could have formulated a similar
statement with $\Sigma A.(P\circ h\circ g)$ as left object.