{X Y} : wedge_pr2 $o (@wedge_inr X Y) $== pmap_idmap. Proof. snrapply Build_pHomotopy. 1: reflexivity. rhs nrapply concat_p1. rhs nrapply concat_p1. rhs nrapply (ap_V _ wglue). exact (inverse2 (wedge_rec_beta_wglue pconst pmap_idmap)^). Defined.
Require Import Basics Types. Require Import Pointed.Core Pointed.pSusp. Require Import Colimits.Pushout. Require Import WildCat. Require Import Homotopy.Suspension.