Require Import HoTT.Basics HoTT.Colimits.Pushout.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Types.Paths Types.Sigma Types.Prod HFiber Limits.Pullback.

(** * 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)
             (spglue' : 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
spglue': 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
spglue': 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
spglue': 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
spglue': 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 spglue'; assumption.
  Defined.

  Definition spushout_rec_beta_spglue (R : Type)
             (spushl' : X -> R) (spushr' : Y -> R)
             (spglue' : forall x y (q : Q x y), spushl' x = spushr' y)
             (x:X) (y:Y) (q:Q x y)
    : ap (spushout_rec R spushl' spushr' spglue') (spglue q) = spglue' x y q
    := Pushout_rec_beta_pglue _ _ _ _ ((x, y); q).

  Definition spushout_ind (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))
    : 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)
spglue': 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)
spglue': 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)
spglue': 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)
spglue': 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 spglue'; assumption.
  Defined.

  Definition spushout_ind_beta_spglue (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.

Definition functor_spushout {X Y Z W : Type}
  {Q : X -> Y -> Type} {Q' : Z -> W -> Type}
  (f : X -> Z) (g : Y -> W) (h : forall x y, Q x y -> Q' (f x) (g y))
  : SPushout Q -> SPushout Q'.
X, Y, Z, W: Type
Q: X -> Y -> Type
Q': Z -> W -> Type
f: X -> Z
g: Y -> W
h: forall (x : X) (y : Y), Q x y -> Q' (f x) (g y)
SPushout Q -> SPushout Q'
Proof.
X, Y, Z, W: Type
Q: X -> Y -> Type
Q': Z -> W -> Type
f: X -> Z
g: Y -> W
h: forall (x : X) (y : Y), Q x y -> Q' (f x) (g y)
SPushout Q -> SPushout Q'
  snapply spushout_rec.
X, Y, Z, W: Type
Q: X -> Y -> Type
Q': Z -> W -> Type
f: X -> Z
g: Y -> W
h: forall (x : X) (y : Y), Q x y -> Q' (f x) (g y)
X -> SPushout Q'
X, Y, Z, W: Type
Q: X -> Y -> Type
Q': Z -> W -> Type
f: X -> Z
g: Y -> W
h: forall (x : X) (y : Y), Q x y -> Q' (f x) (g y)
Y -> SPushout Q'
X, Y, Z, W: Type
Q: X -> Y -> Type
Q': Z -> W -> Type
f: X -> Z
g: Y -> W
h: forall (x : X) (y : Y), Q x y -> Q' (f x) (g y)
forall (x : X) (y : Y),
Q x y -> ?spushl' x = ?spushr' y
  -
X, Y, Z, W: Type
Q: X -> Y -> Type
Q': Z -> W -> Type
f: X -> Z
g: Y -> W
h: forall (x : X) (y : Y), Q x y -> Q' (f x) (g y)
X -> SPushout Q' exact (fun x => spushl Q' (f x)).
  -
X, Y, Z, W: Type
Q: X -> Y -> Type
Q': Z -> W -> Type
f: X -> Z
g: Y -> W
h: forall (x : X) (y : Y), Q x y -> Q' (f x) (g y)
Y -> SPushout Q' exact (fun y => spushr Q' (g y)).
  -
X, Y, Z, W: Type
Q: X -> Y -> Type
Q': Z -> W -> Type
f: X -> Z
g: Y -> W
h: forall (x : X) (y : Y), Q x y -> Q' (f x) (g y)
forall (x : X) (y : Y),
Q x y ->
(fun x0 : X => spushl Q' (f x0)) x =
(fun y0 : Y => spushr Q' (g y0)) y intros x y q.
X, Y, Z, W: Type
Q: X -> Y -> Type
Q': Z -> W -> Type
f: X -> Z
g: Y -> W
h: forall (x : X) (y : Y), Q x y -> Q' (f x) (g y)
x: X
y: Y
q: Q x y
(fun x : X => spushl Q' (f x)) x =
(fun y : Y => spushr Q' (g y)) y apply spglue.
X, Y, Z, W: Type
Q: X -> Y -> Type
Q': Z -> W -> Type
f: X -> Z
g: Y -> W
h: forall (x : X) (y : Y), Q x y -> Q' (f x) (g y)
x: X
y: Y
q: Q x y
Q' (f x) (g y) exact (h x y q).
Defined.

Definition functor_spushout_compose {X Y X' Y' X'' Y'' : Type}
  {Q : X -> Y -> Type} {Q' : X' -> Y' -> Type} {Q'' : X'' -> Y'' -> Type}
  (f : X -> X') (g : Y -> Y') (f' : X' -> X'') (g' : Y' -> Y'')
  (h : forall x y, Q x y -> Q' (f x) (g y))
  (h' : forall x y, Q' x y -> Q'' (f' x) (g' y))
  : functor_spushout f' g' h' o functor_spushout f g h
    == functor_spushout (f' o f) (g' o g) (fun x y => h' _ _ o h x y).
X, Y, X', Y', X'', Y'': Type
Q: X -> Y -> Type
Q': X' -> Y' -> Type
Q'': X'' -> Y'' -> Type
f: X -> X'
g: Y -> Y'
f': X' -> X''
g': Y' -> Y''
h: forall (x : X) (y : Y), Q x y -> Q' (f x) (g y)
h': forall (x : X') (y : Y'),
Q' x y -> Q'' (f' x) (g' y)
functor_spushout f' g' h' o functor_spushout f g h ==
functor_spushout (f' o f) (g' o g)
  (fun (x : X) (y : Y) => h' (f x) (g y) o h x y)
Proof.
X, Y, X', Y', X'', Y'': Type
Q: X -> Y -> Type
Q': X' -> Y' -> Type
Q'': X'' -> Y'' -> Type
f: X -> X'
g: Y -> Y'
f': X' -> X''
g': Y' -> Y''
h: forall (x : X) (y : Y), Q x y -> Q' (f x) (g y)
h': forall (x : X') (y : Y'),
Q' x y -> Q'' (f' x) (g' y)
functor_spushout f' g' h' o functor_spushout f g h ==
functor_spushout (f' o f) (g' o g)
  (fun (x : X) (y : Y) => h' (f x) (g y) o h x y)
  snapply spushout_ind.
X, Y, X', Y', X'', Y'': Type
Q: X -> Y -> Type
Q': X' -> Y' -> Type
Q'': X'' -> Y'' -> Type
f: X -> X'
g: Y -> Y'
f': X' -> X''
g': Y' -> Y''
h: forall (x : X) (y : Y), Q x y -> Q' (f x) (g y)
h': forall (x : X') (y : Y'),
Q' x y -> Q'' (f' x) (g' y)
forall x : X,
(fun p : SPushout Q =>
 (functor_spushout f' g' h' o functor_spushout f g h)
   p =
 functor_spushout (f' o f) (g' o g)
   (fun (x0 : X) (y : Y) => h' (f x0) (g y) o h x0 y)
   p) (spushl Q x)
X, Y, X', Y', X'', Y'': Type
Q: X -> Y -> Type
Q': X' -> Y' -> Type
Q'': X'' -> Y'' -> Type
f: X -> X'
g: Y -> Y'
f': X' -> X''
g': Y' -> Y''
h: forall (x : X) (y : Y), Q x y -> Q' (f x) (g y)
h': forall (x : X') (y : Y'),
Q' x y -> Q'' (f' x) (g' y)
forall y : Y,
(fun p : SPushout Q =>
 (functor_spushout f' g' h' o functor_spushout f g h)
   p =
 functor_spushout (f' o f) (g' o g)
   (fun (x : X) (y0 : Y) => h' (f x) (g y0) o h x y0)
   p) (spushr Q y)
X, Y, X', Y', X'', Y'': Type
Q: X -> Y -> Type
Q': X' -> Y' -> Type
Q'': X'' -> Y'' -> Type
f: X -> X'
g: Y -> Y'
f': X' -> X''
g': Y' -> Y''
h: forall (x : X) (y : Y), Q x y -> Q' (f x) (g y)
h': forall (x : X') (y : Y'),
Q' x y -> Q'' (f' x) (g' y)
forall (x : X) (y : Y) (q : Q x y),
transport
  (fun p : SPushout Q =>
   (functor_spushout f' g' h' o functor_spushout f g h)
     p =
   functor_spushout (f' o f) (g' o g)
     (fun (x0 : X) (y0 : Y) =>
      h' (f x0) (g y0) o h x0 y0) p) (spglue Q q)
  (?spushl' x) = ?spushr' y
  1,2: reflexivity.
X, Y, X', Y', X'', Y'': Type
Q: X -> Y -> Type
Q': X' -> Y' -> Type
Q'': X'' -> Y'' -> Type
f: X -> X'
g: Y -> Y'
f': X' -> X''
g': Y' -> Y''
h: forall (x : X) (y : Y), Q x y -> Q' (f x) (g y)
h': forall (x : X') (y : Y'),
Q' x y -> Q'' (f' x) (g' y)
forall (x : X) (y : Y) (q : Q x y),
transport
  (fun p : SPushout Q =>
   (functor_spushout f' g' h' o functor_spushout f g h)
     p =
   functor_spushout (f' o f) (g' o g)
     (fun (x0 : X) (y0 : Y) =>
      h' (f x0) (g y0) o h x0 y0) p) (spglue Q q)
  ((fun x0 : X => 1) x) = (fun y0 : Y => 1) y
  intros x y q; cbn beta.
X, Y, X', Y', X'', Y'': Type
Q: X -> Y -> Type
Q': X' -> Y' -> Type
Q'': X'' -> Y'' -> Type
f: X -> X'
g: Y -> Y'
f': X' -> X''
g': Y' -> Y''
h: forall (x : X) (y : Y), Q x y -> Q' (f x) (g y)
h': forall (x : X') (y : Y'),
Q' x y -> Q'' (f' x) (g' y)
x: X
y: Y
q: Q x y
transport
  (fun p : SPushout Q =>
   functor_spushout f' g' h'
     (functor_spushout f g h p) =
   functor_spushout (fun x : X => f' (f x))
     (fun x : Y => g' (g x))
     (fun (x : X) (y : Y) (x0 : Q x y) =>
      h' (f x) (g y) (h x y x0)) p) (spglue Q q) 1 = 1
  transport_paths FFlFr.
X, Y, X', Y', X'', Y'': Type
Q: X -> Y -> Type
Q': X' -> Y' -> Type
Q'': X'' -> Y'' -> Type
f: X -> X'
g: Y -> Y'
f': X' -> X''
g': Y' -> Y''
h: forall (x : X) (y : Y), Q x y -> Q' (f x) (g y)
h': forall (x : X') (y : Y'),
Q' x y -> Q'' (f' x) (g' y)
x: X
y: Y
q: Q x y
ap (functor_spushout f' g' h')
  (ap (functor_spushout f g h) (spglue Q q)) @ 1 =
1 @
ap
  (functor_spushout (fun x : X => f' (f x))
     (fun x : Y => g' (g x))
     (fun (x : X) (y : Y) (x0 : Q x y) =>
      h' (f x) (g y) (h x y x0))) (spglue Q q)
  apply equiv_p1_1q.
X, Y, X', Y', X'', Y'': Type
Q: X -> Y -> Type
Q': X' -> Y' -> Type
Q'': X'' -> Y'' -> Type
f: X -> X'
g: Y -> Y'
f': X' -> X''
g': Y' -> Y''
h: forall (x : X) (y : Y), Q x y -> Q' (f x) (g y)
h': forall (x : X') (y : Y'),
Q' x y -> Q'' (f' x) (g' y)
x: X
y: Y
q: Q x y
ap (functor_spushout f' g' h')
  (ap (functor_spushout f g h) (spglue Q q)) =
ap
  (functor_spushout (fun x : X => f' (f x))
     (fun x : Y => g' (g x))
     (fun (x : X) (y : Y) (x0 : Q x y) =>
      h' (f x) (g y) (h x y x0))) (spglue Q q)
  lhs napply ap.
X, Y, X', Y', X'', Y'': Type
Q: X -> Y -> Type
Q': X' -> Y' -> Type
Q'': X'' -> Y'' -> Type
f: X -> X'
g: Y -> Y'
f': X' -> X''
g': Y' -> Y''
h: forall (x : X) (y : Y), Q x y -> Q' (f x) (g y)
h': forall (x : X') (y : Y'),
Q' x y -> Q'' (f' x) (g' y)
x: X
y: Y
q: Q x y
ap (functor_spushout f g h) (spglue Q q) = ?Goal
X, Y, X', Y', X'', Y'': Type
Q: X -> Y -> Type
Q': X' -> Y' -> Type
Q'': X'' -> Y'' -> Type
f: X -> X'
g: Y -> Y'
f': X' -> X''
g': Y' -> Y''
h: forall (x : X) (y : Y), Q x y -> Q' (f x) (g y)
h': forall (x : X') (y : Y'),
Q' x y -> Q'' (f' x) (g' y)
x: X
y: Y
q: Q x y
ap (functor_spushout f' g' h') ?Goal =
ap
  (functor_spushout (fun x : X => f' (f x))
     (fun x : Y => g' (g x))
     (fun (x : X) (y : Y) (x0 : Q x y) =>
      h' (f x) (g y) (h x y x0))) (spglue Q q)
  1: napply spushout_rec_beta_spglue.
X, Y, X', Y', X'', Y'': Type
Q: X -> Y -> Type
Q': X' -> Y' -> Type
Q'': X'' -> Y'' -> Type
f: X -> X'
g: Y -> Y'
f': X' -> X''
g': Y' -> Y''
h: forall (x : X) (y : Y), Q x y -> Q' (f x) (g y)
h': forall (x : X') (y : Y'),
Q' x y -> Q'' (f' x) (g' y)
x: X
y: Y
q: Q x y
ap (functor_spushout f' g' h') (spglue Q' (h x y q)) =
ap
  (functor_spushout (fun x : X => f' (f x))
     (fun x : Y => g' (g x))
     (fun (x : X) (y : Y) (x0 : Q x y) =>
      h' (f x) (g y) (h x y x0))) (spglue Q q)
  lhs napply spushout_rec_beta_spglue.
X, Y, X', Y', X'', Y'': Type
Q: X -> Y -> Type
Q': X' -> Y' -> Type
Q'': X'' -> Y'' -> Type
f: X -> X'
g: Y -> Y'
f': X' -> X''
g': Y' -> Y''
h: forall (x : X) (y : Y), Q x y -> Q' (f x) (g y)
h': forall (x : X') (y : Y'),
Q' x y -> Q'' (f' x) (g' y)
x: X
y: Y
q: Q x y
spglue Q'' (h' (f x) (g y) (h x y q)) =
ap
  (functor_spushout (fun x : X => f' (f x))
     (fun x : Y => g' (g x))
     (fun (x : X) (y : Y) (x0 : Q x y) =>
      h' (f x) (g y) (h x y x0))) (spglue Q q)
  symmetry.
X, Y, X', Y', X'', Y'': Type
Q: X -> Y -> Type
Q': X' -> Y' -> Type
Q'': X'' -> Y'' -> Type
f: X -> X'
g: Y -> Y'
f': X' -> X''
g': Y' -> Y''
h: forall (x : X) (y : Y), Q x y -> Q' (f x) (g y)
h': forall (x : X') (y : Y'),
Q' x y -> Q'' (f' x) (g' y)
x: X
y: Y
q: Q x y
ap
  (functor_spushout (fun x : X => f' (f x))
     (fun x : Y => g' (g x))
     (fun (x : X) (y : Y) (x0 : Q x y) =>
      h' (f x) (g y) (h x y x0))) (spglue Q q) =
spglue Q'' (h' (f x) (g y) (h x y q))
  napply (spushout_rec_beta_spglue Q).
Defined.

Definition functor_spushout_idmap {X Y : Type} {Q : X -> Y -> Type}
  : functor_spushout idmap idmap (fun x y (q : Q x y) => q) == idmap.
X, Y: Type
Q: X -> Y -> Type
functor_spushout idmap idmap
  (fun (x : X) (y : Y) => idmap) == idmap
Proof.
X, Y: Type
Q: X -> Y -> Type
functor_spushout idmap idmap
  (fun (x : X) (y : Y) => idmap) == idmap
  snapply spushout_ind.
X, Y: Type
Q: X -> Y -> Type
forall x : X,
(fun p : SPushout Q =>
 functor_spushout idmap idmap
   (fun (x0 : X) (y : Y) => idmap) p = idmap p)
  (spushl Q x)
X, Y: Type
Q: X -> Y -> Type
forall y : Y,
(fun p : SPushout Q =>
 functor_spushout idmap idmap
   (fun (x : X) (y0 : Y) => idmap) p = idmap p)
  (spushr Q y)
X, Y: Type
Q: X -> Y -> Type
forall (x : X) (y : Y) (q : Q x y),
transport
  (fun p : SPushout Q =>
   functor_spushout idmap idmap
     (fun (x0 : X) (y0 : Y) => idmap) p = idmap p)
  (spglue Q q) (?spushl' x) = ?spushr' y
  1,2: reflexivity.
X, Y: Type
Q: X -> Y -> Type
forall (x : X) (y : Y) (q : Q x y),
transport
  (fun p : SPushout Q =>
   functor_spushout idmap idmap
     (fun (x0 : X) (y0 : Y) => idmap) p = idmap p)
  (spglue Q q) ((fun x0 : X => 1) x) =
(fun y0 : Y => 1) y
  intros x y q; cbn.
X, Y: Type
Q: X -> Y -> Type
x: X
y: Y
q: Q x y
transport
  (fun p : SPushout Q =>
   functor_spushout idmap idmap
     (fun (x : X) (y : Y) => idmap) p = p)
  (spglue Q q) 1 = 1
  transport_paths Flr.
X, Y: Type
Q: X -> Y -> Type
x: X
y: Y
q: Q x y
ap
  (functor_spushout idmap idmap
     (fun (x : X) (y : Y) => idmap)) (spglue Q q) @ 1 =
1 @ spglue Q q
  apply equiv_p1_1q.
X, Y: Type
Q: X -> Y -> Type
x: X
y: Y
q: Q x y
ap
  (functor_spushout idmap idmap
     (fun (x : X) (y : Y) => idmap)) (spglue Q q) =
spglue Q q
  napply spushout_rec_beta_spglue.
Defined.

Definition functor_spushout_homotopic {X Y Z W : Type}
  {Q : X -> Y -> Type} {Q' : Z -> W -> Type}
  {f g : X -> Z} (h : f == g)
  {i j : Y -> W} (k : i == j)
  (l : forall x y, Q x y -> Q' (f x) (i y))
  (m : forall x y, Q x y -> Q' (g x) (j y))
  (H : forall x y q,
    spglue Q' (l x y q) @ ap (spushr Q') (k y)
      = ap (spushl Q') (h x) @ spglue Q' (m x y q))
  : functor_spushout f i l == functor_spushout g j m.
X, Y, Z, W: Type
Q: X -> Y -> Type
Q': Z -> W -> Type
f, g: X -> Z
h: f == g
i, j: Y -> W
k: i == j
l: forall (x : X) (y : Y), Q x y -> Q' (f x) (i y)
m: forall (x : X) (y : Y), Q x y -> Q' (g x) (j y)
H: forall (x : X) (y : Y) (q : Q x y),
spglue Q' (l x y q) @ ap (spushr Q') (k y) =
ap (spushl Q') (h x) @ spglue Q' (m x y q)
functor_spushout f i l == functor_spushout g j m
Proof.
X, Y, Z, W: Type
Q: X -> Y -> Type
Q': Z -> W -> Type
f, g: X -> Z
h: f == g
i, j: Y -> W
k: i == j
l: forall (x : X) (y : Y), Q x y -> Q' (f x) (i y)
m: forall (x : X) (y : Y), Q x y -> Q' (g x) (j y)
H: forall (x : X) (y : Y) (q : Q x y),
spglue Q' (l x y q) @ ap (spushr Q') (k y) =
ap (spushl Q') (h x) @ spglue Q' (m x y q)
functor_spushout f i l == functor_spushout g j m
  snapply spushout_ind.
X, Y, Z, W: Type
Q: X -> Y -> Type
Q': Z -> W -> Type
f, g: X -> Z
h: f == g
i, j: Y -> W
k: i == j
l: forall (x : X) (y : Y), Q x y -> Q' (f x) (i y)
m: forall (x : X) (y : Y), Q x y -> Q' (g x) (j y)
H: forall (x : X) (y : Y) (q : Q x y),
spglue Q' (l x y q) @ ap (spushr Q') (k y) =
ap (spushl Q') (h x) @ spglue Q' (m x y q)
forall x : X,
(fun p : SPushout Q =>
 functor_spushout f i l p = functor_spushout g j m p)
  (spushl Q x)
X, Y, Z, W: Type
Q: X -> Y -> Type
Q': Z -> W -> Type
f, g: X -> Z
h: f == g
i, j: Y -> W
k: i == j
l: forall (x : X) (y : Y), Q x y -> Q' (f x) (i y)
m: forall (x : X) (y : Y), Q x y -> Q' (g x) (j y)
H: forall (x : X) (y : Y) (q : Q x y),
spglue Q' (l x y q) @ ap (spushr Q') (k y) =
ap (spushl Q') (h x) @ spglue Q' (m x y q)
forall y : Y,
(fun p : SPushout Q =>
 functor_spushout f i l p = functor_spushout g j m p)
  (spushr Q y)
X, Y, Z, W: Type
Q: X -> Y -> Type
Q': Z -> W -> Type
f, g: X -> Z
h: f == g
i, j: Y -> W
k: i == j
l: forall (x : X) (y : Y), Q x y -> Q' (f x) (i y)
m: forall (x : X) (y : Y), Q x y -> Q' (g x) (j y)
H: forall (x : X) (y : Y) (q : Q x y),
spglue Q' (l x y q) @ ap (spushr Q') (k y) =
ap (spushl Q') (h x) @ spglue Q' (m x y q)
forall (x : X) (y : Y) (q : Q x y),
transport
  (fun p : SPushout Q =>
   functor_spushout f i l p = functor_spushout g j m p)
  (spglue Q q) (?spushl' x) = ?spushr' y
  -
X, Y, Z, W: Type
Q: X -> Y -> Type
Q': Z -> W -> Type
f, g: X -> Z
h: f == g
i, j: Y -> W
k: i == j
l: forall (x : X) (y : Y), Q x y -> Q' (f x) (i y)
m: forall (x : X) (y : Y), Q x y -> Q' (g x) (j y)
H: forall (x : X) (y : Y) (q : Q x y),
spglue Q' (l x y q) @ ap (spushr Q') (k y) =
ap (spushl Q') (h x) @ spglue Q' (m x y q)
forall x : X,
(fun p : SPushout Q =>
 functor_spushout f i l p = functor_spushout g j m p)
  (spushl Q x) intros x; cbn.
X, Y, Z, W: Type
Q: X -> Y -> Type
Q': Z -> W -> Type
f, g: X -> Z
h: f == g
i, j: Y -> W
k: i == j
l: forall (x : X) (y : Y), Q x y -> Q' (f x) (i y)
m: forall (x : X) (y : Y), Q x y -> Q' (g x) (j y)
H: forall (x : X) (y : Y) (q : Q x y),
spglue Q' (l x y q) @ ap (spushr Q') (k y) =
ap (spushl Q') (h x) @ spglue Q' (m x y q)
x: X
functor_spushout f i l (spushl Q x) =
functor_spushout g j m (spushl Q x)
    exact (ap (spushl Q') (h x)).
  -
X, Y, Z, W: Type
Q: X -> Y -> Type
Q': Z -> W -> Type
f, g: X -> Z
h: f == g
i, j: Y -> W
k: i == j
l: forall (x : X) (y : Y), Q x y -> Q' (f x) (i y)
m: forall (x : X) (y : Y), Q x y -> Q' (g x) (j y)
H: forall (x : X) (y : Y) (q : Q x y),
spglue Q' (l x y q) @ ap (spushr Q') (k y) =
ap (spushl Q') (h x) @ spglue Q' (m x y q)
forall y : Y,
(fun p : SPushout Q =>
 functor_spushout f i l p = functor_spushout g j m p)
  (spushr Q y) intros y; cbn.
X, Y, Z, W: Type
Q: X -> Y -> Type
Q': Z -> W -> Type
f, g: X -> Z
h: f == g
i, j: Y -> W
k: i == j
l: forall (x : X) (y : Y), Q x y -> Q' (f x) (i y)
m: forall (x : X) (y : Y), Q x y -> Q' (g x) (j y)
H: forall (x : X) (y : Y) (q : Q x y),
spglue Q' (l x y q) @ ap (spushr Q') (k y) =
ap (spushl Q') (h x) @ spglue Q' (m x y q)
y: Y
functor_spushout f i l (spushr Q y) =
functor_spushout g j m (spushr Q y)
    exact (ap (spushr Q') (k y)).
  -
X, Y, Z, W: Type
Q: X -> Y -> Type
Q': Z -> W -> Type
f, g: X -> Z
h: f == g
i, j: Y -> W
k: i == j
l: forall (x : X) (y : Y), Q x y -> Q' (f x) (i y)
m: forall (x : X) (y : Y), Q x y -> Q' (g x) (j y)
H: forall (x : X) (y : Y) (q : Q x y),
spglue Q' (l x y q) @ ap (spushr Q') (k y) =
ap (spushl Q') (h x) @ spglue Q' (m x y q)
forall (x : X) (y : Y) (q : Q x y),
transport
  (fun p : SPushout Q =>
   functor_spushout f i l p = functor_spushout g j m p)
  (spglue Q q)
  ((fun x0 : X =>
    ap (spushl Q') (h x0)
    :
    (fun p : SPushout Q =>
     functor_spushout f i l p =
     functor_spushout g j m p) (spushl Q x0)) x) =
(fun y0 : Y =>
 ap (spushr Q') (k y0)
 :
 (fun p : SPushout Q =>
  functor_spushout f i l p = functor_spushout g j m p)
   (spushr Q y0)) y intros x y q.
X, Y, Z, W: Type
Q: X -> Y -> Type
Q': Z -> W -> Type
f, g: X -> Z
h: f == g
i, j: Y -> W
k: i == j
l: forall (x : X) (y : Y), Q x y -> Q' (f x) (i y)
m: forall (x : X) (y : Y), Q x y -> Q' (g x) (j y)
H: forall (x : X) (y : Y) (q : Q x y),
spglue Q' (l x y q) @ ap (spushr Q') (k y) =
ap (spushl Q') (h x) @ spglue Q' (m x y q)
x: X
y: Y
q: Q x y
transport
  (fun p : SPushout Q =>
   functor_spushout f i l p = functor_spushout g j m p)
  (spglue Q q)
  ((fun x : X =>
    ap (spushl Q') (h x)
    :
    (fun p : SPushout Q =>
     functor_spushout f i l p =
     functor_spushout g j m p) (spushl Q x)) x) =
(fun y : Y =>
 ap (spushr Q') (k y)
 :
 (fun p : SPushout Q =>
  functor_spushout f i l p = functor_spushout g j m p)
   (spushr Q y)) y
    transport_paths FlFr.
X, Y, Z, W: Type
Q: X -> Y -> Type
Q': Z -> W -> Type
f, g: X -> Z
h: f == g
i, j: Y -> W
k: i == j
l: forall (x : X) (y : Y), Q x y -> Q' (f x) (i y)
m: forall (x : X) (y : Y), Q x y -> Q' (g x) (j y)
H: forall (x : X) (y : Y) (q : Q x y),
spglue Q' (l x y q) @ ap (spushr Q') (k y) =
ap (spushl Q') (h x) @ spglue Q' (m x y q)
x: X
y: Y
q: Q x y
ap (functor_spushout f i l) (spglue Q q) @
ap (spushr Q') (k y) =
ap (spushl Q') (h x) @
ap (functor_spushout g j m) (spglue Q q)
    lhs napply whiskerR.
X, Y, Z, W: Type
Q: X -> Y -> Type
Q': Z -> W -> Type
f, g: X -> Z
h: f == g
i, j: Y -> W
k: i == j
l: forall (x : X) (y : Y), Q x y -> Q' (f x) (i y)
m: forall (x : X) (y : Y), Q x y -> Q' (g x) (j y)
H: forall (x : X) (y : Y) (q : Q x y),
spglue Q' (l x y q) @ ap (spushr Q') (k y) =
ap (spushl Q') (h x) @ spglue Q' (m x y q)
x: X
y: Y
q: Q x y
ap (functor_spushout f i l) (spglue Q q) = ?Goal
X, Y, Z, W: Type
Q: X -> Y -> Type
Q': Z -> W -> Type
f, g: X -> Z
h: f == g
i, j: Y -> W
k: i == j
l: forall (x : X) (y : Y), Q x y -> Q' (f x) (i y)
m: forall (x : X) (y : Y), Q x y -> Q' (g x) (j y)
H: forall (x : X) (y : Y) (q : Q x y),
spglue Q' (l x y q) @ ap (spushr Q') (k y) =
ap (spushl Q') (h x) @ spglue Q' (m x y q)
x: X
y: Y
q: Q x y
?Goal @ ap (spushr Q') (k y) =
ap (spushl Q') (h x) @
ap (functor_spushout g j m) (spglue Q q)
    1: apply spushout_rec_beta_spglue.
X, Y, Z, W: Type
Q: X -> Y -> Type
Q': Z -> W -> Type
f, g: X -> Z
h: f == g
i, j: Y -> W
k: i == j
l: forall (x : X) (y : Y), Q x y -> Q' (f x) (i y)
m: forall (x : X) (y : Y), Q x y -> Q' (g x) (j y)
H: forall (x : X) (y : Y) (q : Q x y),
spglue Q' (l x y q) @ ap (spushr Q') (k y) =
ap (spushl Q') (h x) @ spglue Q' (m x y q)
x: X
y: Y
q: Q x y
spglue Q' (l x y q) @ ap (spushr Q') (k y) =
ap (spushl Q') (h x) @
ap (functor_spushout g j m) (spglue Q q)
    rhs napply whiskerL.
X, Y, Z, W: Type
Q: X -> Y -> Type
Q': Z -> W -> Type
f, g: X -> Z
h: f == g
i, j: Y -> W
k: i == j
l: forall (x : X) (y : Y), Q x y -> Q' (f x) (i y)
m: forall (x : X) (y : Y), Q x y -> Q' (g x) (j y)
H: forall (x : X) (y : Y) (q : Q x y),
spglue Q' (l x y q) @ ap (spushr Q') (k y) =
ap (spushl Q') (h x) @ spglue Q' (m x y q)
x: X
y: Y
q: Q x y
spglue Q' (l x y q) @ ap (spushr Q') (k y) =
ap (spushl Q') (h x) @ ?Goal
X, Y, Z, W: Type
Q: X -> Y -> Type
Q': Z -> W -> Type
f, g: X -> Z
h: f == g
i, j: Y -> W
k: i == j
l: forall (x : X) (y : Y), Q x y -> Q' (f x) (i y)
m: forall (x : X) (y : Y), Q x y -> Q' (g x) (j y)
H: forall (x : X) (y : Y) (q : Q x y),
spglue Q' (l x y q) @ ap (spushr Q') (k y) =
ap (spushl Q') (h x) @ spglue Q' (m x y q)
x: X
y: Y
q: Q x y
ap (functor_spushout g j m) (spglue Q q) = ?Goal
    2: apply spushout_rec_beta_spglue.
X, Y, Z, W: Type
Q: X -> Y -> Type
Q': Z -> W -> Type
f, g: X -> Z
h: f == g
i, j: Y -> W
k: i == j
l: forall (x : X) (y : Y), Q x y -> Q' (f x) (i y)
m: forall (x : X) (y : Y), Q x y -> Q' (g x) (j y)
H: forall (x : X) (y : Y) (q : Q x y),
spglue Q' (l x y q) @ ap (spushr Q') (k y) =
ap (spushl Q') (h x) @ spglue Q' (m x y q)
x: X
y: Y
q: Q x y
spglue Q' (l x y q) @ ap (spushr Q') (k y) =
ap (spushl Q') (h x) @ spglue Q' (m x y q)
    apply H.
Defined.

(** Any pushout is equivalent to a span pushout. *)
Definition equiv_pushout_spushout {X Y Z : Type} (f : X -> Y) (g : X -> Z)
  : Pushout f g
    <~> SPushout (fun (y : Y) (z : Z) => {x : X & f x = y /\ g x = z}).
X, Y, Z: Type
f: X -> Y
g: X -> Z
Pushout f g <~>
SPushout
  (fun (y : Y) (z : Z) =>
   {x : X & (f x = y) * (g x = z)})
Proof.
X, Y, Z: Type
f: X -> Y
g: X -> Z
Pushout f g <~>
SPushout
  (fun (y : Y) (z : Z) =>
   {x : X & (f x = y) * (g x = z)})
  snapply equiv_pushout.
X, Y, Z: Type
f: X -> Y
g: X -> Z
X <~>
{xy : Y * Z &
(fun (y : Y) (z : Z) =>
 {x : X & (f x = y) * (g x = z)}) (fst xy) (snd xy)}
X, Y, Z: Type
f: X -> Y
g: X -> Z
Y <~> Y
X, Y, Z: Type
f: X -> Y
g: X -> Z
Z <~> Z
X, Y, Z: Type
f: X -> Y
g: X -> Z
?eB o f ==
(fun
   x : {xy : Y * Z &
       (fun (y : Y) (z : Z) =>
        {x : X & (f x = y) * (g x = z)}) (fst xy)
         (snd xy)} => fst x.1) o ?eA
X, Y, Z: Type
f: X -> Y
g: X -> Z
?eC o g ==
(fun
   x : {xy : Y * Z &
       (fun (y : Y) (z : Z) =>
        {x : X & (f x = y) * (g x = z)}) (fst xy)
         (snd xy)} => snd x.1) o ?eA
  {
X, Y, Z: Type
f: X -> Y
g: X -> Z
X <~>
{xy : Y * Z &
(fun (y : Y) (z : Z) =>
 {x : X & (f x = y) * (g x = z)}) (fst xy) (snd xy)} nrefine (equiv_sigma_prod _ oE _).
X, Y, Z: Type
f: X -> Y
g: X -> Z
X <~>
{a : Y &
{b : Z &
{x : X & (f x = fst (a, b)) * (g x = snd (a, b))}}}
    apply equiv_double_fibration_replacement. }
X, Y, Z: Type
f: X -> Y
g: X -> Z
Y <~> Y
X, Y, Z: Type
f: X -> Y
g: X -> Z
Z <~> Z
X, Y, Z: Type
f: X -> Y
g: X -> Z
?eB o f ==
(fun
   x : {xy : Y * Z &
       (fun (y : Y) (z : Z) =>
        {x : X & (f x = y) * (g x = z)}) (fst xy)
         (snd xy)} => fst x.1)
o (equiv_sigma_prod
     (fun xy : Y * Z =>
      (fun (y : Y) (z : Z) =>
       {x : X & (f x = y) * (g x = z)}) (fst xy)
        (snd xy))
   oE equiv_double_fibration_replacement f g)
X, Y, Z: Type
f: X -> Y
g: X -> Z
?eC o g ==
(fun
   x : {xy : Y * Z &
       (fun (y : Y) (z : Z) =>
        {x : X & (f x = y) * (g x = z)}) (fst xy)
         (snd xy)} => snd x.1)
o (equiv_sigma_prod
     (fun xy : Y * Z =>
      (fun (y : Y) (z : Z) =>
       {x : X & (f x = y) * (g x = z)}) (fst xy)
        (snd xy))
   oE equiv_double_fibration_replacement f g)
  1-4: reflexivity.
Defined.

(** There is a natural map from the total space of [Q] to the pushout product of [Q]. *)
Definition spushout_sjoin_map {X Y : Type} (Q : X -> Y -> Type)
  : {x : X & {y : Y & Q x y}} -> Pullback (spushl Q) (spushr Q)
  := functor_sigma idmap (fun _ => functor_sigma idmap (fun _ => spglue Q)).