{A B C} (f : A -> B) (g : A -> C) P (e : Pushout f g -> P) : Pushout_rec P (e o pushl) (e o pushr) (fun a => ap e (pglue a)) == e. Proof. snrapply Pushout_ind. 1, 2: reflexivity. intro a; cbn beta. apply transport_paths_FlFr'. apply equiv_p1_1q. nrapply Pushout_rec_beta_pglue. Defined.
Require Import Basics. Require Import Types.Paths Types.Arrow Types.Sigma Types.Sum Types.Universe.