{n : trunc_index} {X : Type} (HX : forall (f : Sphere n.+2 -> X), NullHomotopy f) {struct n} : IsTrunc n.+1 X. Proof. destruct n as [ | n']. - apply hprop_allpath. intros x0 x1. set (f := (fun b => if (S0_to_Bool b) then x0 else x1)). set (n := HX f). exact (n.2 North @ (n.2 South)^). - apply istrunc_S; intros x0 x1. apply ( n'). intro f. apply nullhomot_paths_from_susp, HX. 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.