利用镜面空间在同类型论中解环群

在同类型论的框架下，每个类型都可以解释为一个空间。此外，给定一个类型的一个元素，即相应空间中的一个点，可以定义另一个编码以该点为基点的环空间的类型。特别地，当我们开始的类型是群模型时，这个环空间始终是一个群。相反地，对于每一个群，我们可以关联一个类型（更准确地说，一个指向的连通群模型），其环空间就是这个群：这一操作称为解环。构造此类群解环的通用程序（基于torsor，或基于将Eilenberg-MacLane空间描述为更高演绎类型的描述）都带有消除原则，这些原则并不直接允许消除到未截断的类型，因此在实践中难以使用。本文构造了循环群$\mathbb{Z}_m$的解环，这些解环是细胞结构的，因此不受此缺陷的影响。为此，我们提供了镜面空间的类型论实现，这些空间构成代数拓扑学中重要的空间族。我们的定义基于计算从圆到任意$\mathbb{Z}_m$解环的某些映射的迭代连接。从本质上说，这项工作推广了Buchholtz和Rijke的构造，后者处理m=2的情况，尽管一般情况需要更复杂的工具。最后，我们利用这一构造也提供了二面体群的细胞描述，并解释我们如何希望利用这些来计算这些群的上同调和更高作用。