(P : pushout_assoc_left -> Type) (pushb : forall b, P (pushll b)) (pushc : forall c, P (pushlm c)) (pushd : forall d, P (pushlr d)) (pusha1 : forall a1, (pgluell a1) # pushb (f1 a1) = pushc (g1 a1)) (pusha2 : forall a2, (pgluelr a2) # pushc (f2 a2) = pushd (g2 a2)) : forall x, P x. Proof. srefine (Pushout_ind _ _ pushd _). - srefine (Pushout_ind _ pushb pushc _). intros a1. exact (transport_compose P pushl _ _ @ pusha1 a1). - exact pusha2. Defined.
Require Import Basics. Require Import Types.Paths Types.Arrow Types.Sigma Types.Sum Types.Universe.