fact: Fixpoint allnullhomot_trunc {n : trunc_index} {X : Type} `{IsTrunc n X} (f : Sphere n.+1 -> X) {struct n} : NullHomotopy f.
imports: Basics Types WildCat.Equiv NullHomotopy Homotopy.Suspension Pointed Truncations Spaces.Circle Spaces.TwoSphere