  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.
