Library HoTT.Colimits.SpanPushout

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 qpglue ((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.