In the setting of homotopy type theory, each type can be interpreted as a space. Moreover, given an element of a type, i.e. a point in the corresponding space, one can define another type which encodes the space of loops based at this point. In particular, when the type we started with is a groupoid, this loop space is always a group. Conversely, to every group we can associate a type (more precisely, a pointed connected groupoid) whose loop space is this group: this operation is called delooping. The generic procedures for constructing such deloopings of groups (based on torsors, or on descriptions of Eilenberg-MacLane spaces as higher inductive types) are unfortunately equipped with elimination principles which do not directly allow eliminating to untruncated types, and are thus difficult to work with in practice. Here, we construct deloopings of the cyclic groups $\mathbb{Z}_m$ which are cellular, and thus do not suffer from this shortcoming. In order to do so, we provide type-theoretic implementations of lens spaces, which constitute an important family of spaces in algebraic topology. Our definition is based on the computation of an iterative join of suitable maps from the circle to an arbitrary delooping of $\mathbb{Z}_m$. In some sense, this work generalizes the construction of real projective spaces by Buchholtz and Rijke, which handles the case m=2, although the general setting requires more involved tools. Finally, we use this construction to also provide cellular descriptions of dihedral groups, and explain how we can hope to use those to compute the cohomology and higher actions of such groups.

翻译：在同伦类型论框架下，每个类型可解释为一个空间。进一步地，给定某个类型的元素（即对应空间中的一点），可定义另一个编码基于该点环路空间的类型。特别地，当初始类型为群胚时，该环路空间总是一个群。反之，对任意群可关联一个类型（更精确地，带基点的连通群胚），其环路空间即为该群：这一操作称为消圈化。基于 torsor 或基于将 Eilenberg-MacLane 空间描述为高阶归纳类型的通用群消圈化构造方法，其消去原则存在缺陷——无法直接消去至非截断类型，因此在实践中难以操作。本文针对循环群 $\mathbb{Z}_m$ 构造了细胞式消圈化，从而避免了这一局限性。为此，我们提供了透镜空间的类型论实现——透镜空间是代数拓扑中的重要空间族。我们的定义基于从圆环到任意 $\mathbb{Z}_m$ 消圈化的适当映射的迭代连接计算。从某种意义上，本工作推广了 Buchholtz 与 Rijke 关于实射影空间（处理 m=2 情形）的构造，但一般情形需要更复杂的工具。最后，我们利用该构造为二面体群提供细胞化描述，并阐释了如何利用这些结果计算此类群的上同调与高阶作用。