(R : Type) (spushl' : X -> R) (spushr' : Y -> R) (sglue' : forall x y (q : Q x y), spushl' x = spushr' y) : SPushout -> R. Proof. srapply (@Pushout_rec {xy:X * Y & Q (fst xy) (snd xy)} X Y (fst o pr1) (snd o pr1) R spushl' spushr'). intros [[x y] q]; cbn in *. apply sglue'; assumption. Defined.
Require Import HoTT.Basics HoTT.Colimits.Pushout.