Require Import HoTT.Basics HoTT.Colimits.Pushout.

Section SpanPushout.
  Context {X Y : Type} (Q : X → Y → Type).

  Definition SPushout := @Pushout@{up _ _ up} (sig@{up _} (fun (xy : X × Y) ⇒ Q (fst xy) (snd xy))) X Y
                                  (fst o pr1) (snd o pr1).
  Definition spushl : X → SPushout := pushl.
  Definition spushr : Y → SPushout := pushr.
  Definition spglue {x:X} {y:Y} : Q x y → spushl x = spushr y
    := fun q ⇒ pglue ((x,y) ; q).

  Definition SPushout_rec (R : Type)
             (spushl' : X → R) (spushr' : Y → R)
             (sglue' : ∀ 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.

  Definition SPushout_ind (R : SPushout → Type)
             (spushl' : ∀ x, R (spushl x))
             (spushr' : ∀ y, R (spushr y))
             (sglue' : ∀ x y (q : Q x y),
                 transport R (spglue q) (spushl' x) = (spushr' y))
    : ∀ p, R p.
  Proof.
    srapply (@Pushout_ind {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.

  Definition spushout_ind_beta_sglue (R : SPushout → Type)
             (spushl' : ∀ x, R (spushl x))
             (spushr' : ∀ y, R (spushr y))
             (spglue' : ∀ x y (q : Q x y),
                 transport R (spglue q) (spushl' x) = (spushr' y))
             (x:X) (y:Y) (q:Q x y)
    : apD (SPushout_ind R spushl' spushr' spglue') (spglue q) = spglue' x y q
    := Pushout_ind_beta_pglue _ _ _ _ ((x,y);q).

End SpanPushout.