Search

• < Previous
• 1
• Next >

On the Nielsen-Schreier Theorem in Homotopy Type Theory

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&nbsp;[&hellip;]