  Homotopy type theory is a logical setting based on Martin-L\"of 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, the loop spaces of
types with a distinguished element (more precisely, pointed connected
groupoids), provide a natural representation of groups, what we call here
internal groups. The construction which internalizes a given group is called
delooping, because it is a formal inverse to the loop space operator. As we
recall in the article, this delooping operation has a concrete definition for
any group G given by the type of G-torsors. Those are particular sets together
with an action of G, which means that they come equipped with an endomorphism
for every element of G. We show that, when a generating set is known for the
group, we can construct a smaller representation of the type of G-torsors,
using the fact that we only need automorphisms for the elements of the
generating set. We thus obtain a concise definition of (internal) groups in
homotopy type theory, which can be useful to define deloopings without
resorting to higher inductive types, or to perform computations on those. We
also investigate an abstract construction for the Cayley group of a generated
group. Most of the developments performed in the article have been formalized
using the cubical version of the Agda proof assistant.
