论文标题
在尼尔森 - 雪橇定理上，在同型类型理论中
On the Nielsen-Schreier Theorem in Homotopy Type Theory
论文作者
论文摘要
我们在同型类型理论中使用组呈现组的nielsen-schreier定理（自由组的亚组是免费的，是自由组的亚组）的表述。我们显示了有限索引子组的特殊情况，并从选择的公理中遵循完整的定理。我们举例说明了布尔无限拓扑的示例，在该典范中，我们对定理的表述不持有，并且在同义类型理论中证明了定理的更强的“未截断”版本是错误的。
We give a formulation of the Nielsen-Schreier theorem (subgroups of free groups are free) in homotopy type theory using the presentation of groups as pointed connected 1-truncated types. We show the special case of finite index subgroups holds constructively and the full theorem follows from the axiom of choice. We give an example of a boolean infinity topos where our formulation of the theorem does not hold and show a stronger "untruncated" version of the theorem is provably false in homotopy type theory.
