a2 : ap pushout_assoc_right_rec (pgluerr a2) = pusha2 a2. Proof. unfold pgluerr. rewrite <- (ap_compose (pushr' f1 (pushl' f2 g2 o g1)) pushout_assoc_right_rec). change (ap (Pushout_rec P pushc pushd pusha2) (pglue' f2 g2 a2) = pusha2 a2). apply Pushout_rec_beta_pglue. Defined.
Require Import Basics. Require Import Types.Paths Types.Arrow Types.Sigma Types.Sum Types.Universe.