(P : Type) (pushb : B -> P) (pushc : C -> P) (pusha : forall a : A, pushb (f a) = pushc (g a)) : Pushout_rec P pushb pushc pusha == PO_rec P pushb pushc pusha o equiv_pushout_PO. Proof. snrapply Pushout_ind. 1, 2: reflexivity. intro a; cbn beta. nrapply transport_paths_FlFr'; apply equiv_p1_1q. lhs exact (Pushout_rec_beta_pglue P pushb pushc pusha a). symmetry. lhs nrapply (ap_compose equiv_pushout_PO _ (pglue a)). lhs nrapply (ap _ (equiv_pushout_PO_beta_pglue a)). nrapply PO_rec_beta_pp. Defined.
Require Import Basics. Require Import Types. Require Import Diagrams.Graph. Require Import Diagrams.Diagram. Require Import Diagrams.Span. Require Import Diagrams.Cocone. Require Import Colimits.Colimit. Import Colimits.Pushout.