  We show "free theorems" in the style of Wadler for polymorphic functions in
homotopy type theory as consequences of the abstraction theorem. As an
application, it follows that every space defined as a higher inductive type has
the same homotopy groups as some type of polymorphic functions defined without
univalence or higher inductive types.
