{X} : wedge_pr1 $o psusp_pinch X $== Id (psusp X). Proof. snrapply Build_pHomotopy. - snrapply Susp_ind_FlFr. + reflexivity. + exact (merid pt). + intros x. rhs nrapply concat_1p. rhs nrapply ap_idmap. apply moveR_pM. change (?t = _) with (t = loop_susp_unit X x). lhs nrapply (ap_compose (psusp_pinch X)). lhs nrapply (ap _ (psusp_pinch_beta_merid x)). lhs nrapply ap_pp. lhs nrapply (ap (fun x => _ @ x) (ap_V _ _)). apply moveR_pV. rhs nrapply (whiskerL _ (wedge_rec_beta_wglue _ _)). lhs nrapply ap_pp. lhs nrapply (ap (fun x => _ @ x)). { lhs_V nrapply ap_compose. apply ap_const. } lhs nrapply concat_p1. lhs nrapply ap_pp. lhs nrapply (ap (fun x => _ @ x) (wedge_rec_beta_wglue _ _)). f_ap. lhs_V nrapply (ap_compose wedge_inl). apply ap_idmap. - reflexivity. Defined.
Require Import Basics Types. Require Import Pointed.Core Pointed.pSusp. Require Import Colimits.Pushout. Require Import WildCat. Require Import Homotopy.Suspension.