{X Z : Type} (H_N H_S : Z) (f : X -> H_N = H_S) (n : NullHomotopy (Susp_rec H_N H_S f)) : NullHomotopy f. Proof. exists (n.2 North @ (n.2 South)^). intro x. apply moveL_pV. transitivity (ap (Susp_rec H_N H_S f) (merid x) @ n.2 South). - apply whiskerR, inverse, Susp_rec_beta_merid. - refine (concat_Ap n.2 (merid x) @ _). apply (concatR (concat_p1 _)), whiskerL. apply ap_const. Defined.
Require Import Basics. Require Import Types. Require Import Cubical.DPath Cubical.DPathSquare. Require Import WildCat. Require Import Colimits.Pushout. Require Import NullHomotopy. Require Import Truncations.Core. Require Import Modalities.Modality. Require Import Extensions.