{n : trunc_index} {X : Type} `{IsTrunc n X} (f : Sphere n.+1 -> X) {struct n} : NullHomotopy f. Proof. destruct n as [ | n']. - exists (center X). intros []. - apply nullhomot_susp_from_paths. rapply . Defined.
Require Import Basics Types. Require Import WildCat.Equiv. Require Import NullHomotopy. Require Import Homotopy.Suspension. Require Import Pointed. Require Import Truncations. Require Import Spaces.Circle Spaces.TwoSphere.