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.

翻译：同伦类型理论是一种基于Martin-Löf类型理论的逻辑框架，可在其中以综合方式进行几何构造和证明。具体而言，类型可被解释为空间（在连续形变意义下），而证明则被解释为同伦不变的构造。在此背景下，带有指定基点的类型（更精确地说，是带基点的连通群胚）的环路空间为群提供了自然表示——我们在此称之为内部群。将给定群进行内部化的构造称为反圈操作，因为它形式上构成了环路空间算子之逆。如本文所述，对任意群G而言，该反圈操作具有具体定义：即G-主齐性空间类型。这些是配备G作用的特定集合，意味着每个G元素都对应一个自同态。我们证明，当群的生成集已知时，可以利用仅需生成集元素的自同构这一事实，构造G-主齐性空间类型的更精简表示。由此，我们获得同伦类型理论中（内部）群的紧凑定义，该定义既可用于无需高阶归纳类型定义反圈操作，也可用于实现相关计算。此外，我们还研究了生成群Cayley群的抽象构造。本文大多数推导工作已使用基于立方体版本的Agda证明辅助工具完成形式化验证。