(P : pushout_assoc_right -> Type) (pushb : forall b, P (pushrl b)) (pushc : forall c, P (pushrm c)) (pushd : forall d, P (pushrr d)) (pusha1 : forall a1, (pgluerl a1) # pushb (f1 a1) = pushc (g1 a1)) (pusha2 : forall a2, (pgluerr a2) # pushc (f2 a2) = pushd (g2 a2)) : forall x, P x. Proof. srefine (Pushout_ind _ pushb _ _). - srefine (Pushout_ind _ pushc pushd _). intros a2. exact (transport_compose P pushr _ _ @ pusha2 a2). - exact pusha1. Defined.
Require Import Basics. Require Import Types.Paths Types.Arrow Types.Sigma Types.Sum Types.Universe.