X Y Z (f g : X \/ Y $-> Z) : f $o wedge_inl $== g $o wedge_inl -> f $o wedge_inr $== g $o wedge_inr -> f $== g. Proof. intros p q. snrapply Build_pHomotopy. - snrapply (Pushout_ind _ p q). intros []. nrapply transport_paths_FlFr'. lhs nrapply (whiskerL _ (dpoint_eq q)). rhs nrapply (whiskerR (dpoint_eq p)). clear p q. lhs nrapply concat_p_pp. simpl. apply moveR_pV. lhs nrapply whiskerL. { nrapply whiskerR. apply ap_V. } lhs nrapply concat_p_pp. lhs nrapply whiskerR. 1: apply concat_pV. rhs nrapply concat_p_pp. apply moveL_pM. lhs_V nrapply concat_p1. lhs nrapply concat_pp_p. lhs_V nrapply whiskerL. 1: apply (inv_pp 1). rhs nrapply whiskerL. 2: apply ap_V. apply moveL_pV. reflexivity. - simpl; pelim p q. f_ap. 1: apply concat_1p. lhs nrapply inv_pp. apply concat_p1. Defined.
Require Import Basics Types. Require Import Pointed.Core Pointed.pSusp. Require Import Colimits.Pushout. Require Import WildCat. Require Import Homotopy.Suspension.