Require Import HoTT.Basics HoTT.Colimits.Pushout.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

(** * Pushouts of "dependent spans". *)

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' : forall x y (q : Q x y), spushl' x = spushr' y)
    : SPushout -> R.
X, Y: Type
Q: X -> Y -> Type
R: Type
spushl': X -> R
spushr': Y -> R
sglue': forall (x : X) (y : Y),
Q x y -> spushl' x = spushr' y
SPushout -> R
  Proof.
X, Y: Type
Q: X -> Y -> Type
R: Type
spushl': X -> R
spushr': Y -> R
sglue': forall (x : X) (y : Y),
Q x y -> spushl' x = spushr' y
SPushout -> R
    srapply (@Pushout_rec {xy:X * Y & Q (fst xy) (snd xy)} X Y
                          (fst o pr1) (snd o pr1) R spushl' spushr').
X, Y: Type
Q: X -> Y -> Type
R: Type
spushl': X -> R
spushr': Y -> R
sglue': forall (x : X) (y : Y),
Q x y -> spushl' x = spushr' y
forall a : {xy : X * Y & Q (fst xy) (snd xy)},
spushl' ((fst o pr1) a) = spushr' ((snd o pr1) a)
    intros [[x y] q]; cbn in *.
X, Y: Type
Q: X -> Y -> Type
R: Type
spushl': X -> R
spushr': Y -> R
sglue': forall (x : X) (y : Y),
Q x y -> spushl' x = spushr' y
x: X
y: Y
q: Q x y
spushl' x = spushr' y
    apply sglue'; assumption.
  Defined.

  Definition SPushout_ind (R : SPushout -> Type)
             (spushl' : forall x, R (spushl x))
             (spushr' : forall y, R (spushr y))
             (sglue' : forall x y (q : Q x y), 
                 transport R (spglue q) (spushl' x) = (spushr' y))
    : forall p, R p.
X, Y: Type
Q: X -> Y -> Type
R: SPushout -> Type
spushl': forall x : X, R (spushl x)
spushr': forall y : Y, R (spushr y)
sglue': forall (x : X) (y : Y) 
(q : Q x y),
transport R (spglue q) (spushl' x) =
spushr' y
forall p : SPushout, R p
  Proof.
X, Y: Type
Q: X -> Y -> Type
R: SPushout -> Type
spushl': forall x : X, R (spushl x)
spushr': forall y : Y, R (spushr y)
sglue': forall (x : X) (y : Y) 
(q : Q x y),
transport R (spglue q) (spushl' x) =
spushr' y
forall p : SPushout, R p
    srapply (@Pushout_ind {xy:X * Y & Q (fst xy) (snd xy)} X Y
                          (fst o pr1) (snd o pr1) R spushl' spushr').
X, Y: Type
Q: X -> Y -> Type
R: SPushout -> Type
spushl': forall x : X, R (spushl x)
spushr': forall y : Y, R (spushr y)
sglue': forall (x : X) (y : Y) 
(q : Q x y),
transport R (spglue q) (spushl' x) =
spushr' y
forall a : {xy : X * Y & Q (fst xy) (snd xy)},
transport R (pglue a) (spushl' ((fst o pr1) a)) =
spushr' ((snd o pr1) a)
    intros [[x y] q]; cbn in *.
X, Y: Type
Q: X -> Y -> Type
R: SPushout -> Type
spushl': forall x : X, R (spushl x)
spushr': forall y : Y, R (spushr y)
sglue': forall (x : X) (y : Y) 
(q : Q x y),
transport R (spglue q) (spushl' x) =
spushr' y
x: X
y: Y
q: Q x y
transport R (pglue ((x, y); q)) (spushl' x) =
spushr' y
    apply sglue'; assumption.
  Defined.

  Definition spushout_ind_beta_sglue (R : SPushout -> Type)
             (spushl' : forall x, R (spushl x))
             (spushr' : forall y, R (spushr y))
             (spglue' : forall 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.