(* -*- mode: coq; mode: visual-line -*- *)
Require Import Basics.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Types.Paths Types.Arrow Types.Sigma Types.Sum Types.Universe.
Require Export Colimits.Coeq.

Local Open Scope path_scope.

(** * Homotopy Pushouts *)

(** We define pushouts in terms of coproducts and coequalizers. *)

Definition Pushout@{i j k l} {A : Type@{i}} {B : Type@{j}} {C : Type@{k}}
  (f : A -> B) (g : A -> C) : Type@{l}
  := Coeq@{l l _} (inl o f) (inr o g).

Definition push {A B C : Type} {f : A -> B} {g : A -> C}
 : B+C -> Pushout f g
  := @coeq _ _ (inl o f) (inr o g).

Definition pushl {A B C} {f : A -> B} {g : A -> C} (b : B)
  : Pushout f g := push (inl b).
Definition pushr {A B C} {f : A -> B} {g : A -> C} (c : C)
  : Pushout f g := push (inr c).

Definition pglue {A B C : Type} {f : A -> B} {g : A -> C} (a : A)
  : pushl (f a) = pushr (g a)
  := @cglue A (B+C) (inl o f) (inr o g) a.

(* Some versions with explicit parameters. *)
Definition pushl' {A B C} (f : A -> B) (g : A -> C) (b : B) : Pushout f g := pushl b.
Definition pushr' {A B C} (f : A -> B) (g : A -> C) (c : C) : Pushout f g := pushr c.
Definition pglue' {A B C : Type} (f : A -> B) (g : A -> C) (a : A) : pushl (f a) = pushr (g a)
  := pglue a.

Section PushoutInd.

  Context {A B C : Type} {f : A -> B} {g : A -> C}
    (P : Pushout f g -> Type)
    (pushb : forall b : B, P (pushl b))
    (pushc : forall c : C, P (pushr c))
    (pusha : forall a : A, (pglue a) # (pushb (f a)) = pushc (g a)).

  Definition Pushout_ind
    : forall (w : Pushout f g), P w
    := Coeq_ind P (sum_ind (P o push) pushb pushc) pusha.

  Definition Pushout_ind_beta_pushl (b:B) : Pushout_ind (pushl b) = pushb b
    := 1.
  Definition Pushout_ind_beta_pushr (c:C) : Pushout_ind (pushr c) = pushc c
    := 1.

  Definition Pushout_ind_beta_pglue (a:A)
    : apD Pushout_ind (pglue a) = pusha a
    := Coeq_ind_beta_cglue P (fun bc => match bc with inl b => pushb b | inr c => pushc c end) pusha a.

End PushoutInd.

(** But we want to allow the user to forget that we've defined pushouts in terms of coequalizers. *)
Arguments Pushout : simpl never.
Arguments push : simpl never.
Arguments pglue : simpl never.
Arguments Pushout_ind_beta_pglue : simpl never.
(** However, we do allow [Pushout_ind] to simplify, as it computes on point constructors. *)

Definition Pushout_rec {A B C} {f : A -> B} {g : A -> C} (P : Type)
  (pushb : B -> P)
  (pushc : C -> P)
  (pusha : forall a : A, pushb (f a) = pushc (g a))
  : @Pushout A B C f g -> P
  := @Coeq_rec _ _ (inl o f) (inr o g) P (sum_rec P pushb pushc) pusha.

Definition Pushout_rec_beta_pglue {A B C f g} (P : Type)
  (pushb : B -> P)
  (pushc : C -> P)
  (pusha : forall a : A, pushb (f a) = pushc (g a))
  (a : A)
  : ap (Pushout_rec P pushb pushc pusha) (pglue a) = pusha a.
A, B, C: Type
f: A -> B
g: A -> C
P: Type
pushb: B -> P
pushc: C -> P
pusha: forall a : A, pushb (f a) = pushc (g a)
a: A
ap (Pushout_rec P pushb pushc pusha) (pglue a) =
pusha a
Proof.
A, B, C: Type
f: A -> B
g: A -> C
P: Type
pushb: B -> P
pushc: C -> P
pusha: forall a : A, pushb (f a) = pushc (g a)
a: A
ap (Pushout_rec P pushb pushc pusha) (pglue a) =
pusha a
  nrapply Coeq_rec_beta_cglue.
Defined.

(** ** Universal property *)

Definition pushout_unrec {A B C P} (f : A -> B) (g : A -> C)
           (h : Pushout f g -> P)
  : {psh : (B -> P) * (C -> P) &
           forall a, fst psh (f a) = snd psh (g a)}.
A, B, C, P: Type
f: A -> B
g: A -> C
h: Pushout f g -> P
{psh : (B -> P) * (C -> P) &
forall a : A, fst psh (f a) = snd psh (g a)}
Proof.
A, B, C, P: Type
f: A -> B
g: A -> C
h: Pushout f g -> P
{psh : (B -> P) * (C -> P) &
forall a : A, fst psh (f a) = snd psh (g a)}
  exists (h o pushl, h o pushr).
A, B, C, P: Type
f: A -> B
g: A -> C
h: Pushout f g -> P
forall a : A,
fst
  (fun x : B => h (pushl x), fun x : C => h (pushr x))
  (f a) =
snd
  (fun x : B => h (pushl x), fun x : C => h (pushr x))
  (g a)
  intros a; cbn.
A, B, C, P: Type
f: A -> B
g: A -> C
h: Pushout f g -> P
a: A
h (pushl (f a)) = h (pushr (g a))
  exact (ap h (pglue a)).
Defined.

Definition pushout_rec_unrec {A B C} (f : A -> B) (g : A -> C) P
  (e : Pushout f g -> P)
  : Pushout_rec P (e o pushl) (e o pushr) (fun a => ap e (pglue a)) == e.
A, B, C: Type
f: A -> B
g: A -> C
P: Type
e: Pushout f g -> P
Pushout_rec P (e o pushl) (e o pushr)
  (fun a : A => ap e (pglue a)) == e
Proof.
A, B, C: Type
f: A -> B
g: A -> C
P: Type
e: Pushout f g -> P
Pushout_rec P (e o pushl) (e o pushr)
  (fun a : A => ap e (pglue a)) == e
  snrapply Pushout_ind.
A, B, C: Type
f: A -> B
g: A -> C
P: Type
e: Pushout f g -> P
forall b : B,
(fun w : Pushout f g =>
 Pushout_rec P (e o pushl) (e o pushr)
   (fun a : A => ap e (pglue a)) w = e w) (pushl b)
A, B, C: Type
f: A -> B
g: A -> C
P: Type
e: Pushout f g -> P
forall c : C,
(fun w : Pushout f g =>
 Pushout_rec P (e o pushl) (e o pushr)
   (fun a : A => ap e (pglue a)) w = e w) (pushr c)
A, B, C: Type
f: A -> B
g: A -> C
P: Type
e: Pushout f g -> P
forall a : A,
transport
  (fun w : Pushout f g =>
   Pushout_rec P (e o pushl) (e o pushr)
     (fun a0 : A => ap e (pglue a0)) w = e w)
  (pglue a) (?pushb (f a)) = ?pushc (g a)
  1, 2: reflexivity.
A, B, C: Type
f: A -> B
g: A -> C
P: Type
e: Pushout f g -> P
forall a : A,
transport
  (fun w : Pushout f g =>
   Pushout_rec P (e o pushl) (e o pushr)
     (fun a0 : A => ap e (pglue a0)) w = e w)
  (pglue a) ((fun b : B => 1) (f a)) =
(fun c : C => 1) (g a)
  intro a; cbn beta.
A, B, C: Type
f: A -> B
g: A -> C
P: Type
e: Pushout f g -> P
a: A
transport
  (fun w : Pushout f g =>
   Pushout_rec P (fun x : B => e (pushl x))
     (fun x : C => e (pushr x))
     (fun a : A => ap e (pglue a)) w = e w) (pglue a)
  1 = 1
  apply transport_paths_FlFr'.
A, B, C: Type
f: A -> B
g: A -> C
P: Type
e: Pushout f g -> P
a: A
ap
  (Pushout_rec P (fun x : B => e (pushl x))
     (fun x : C => e (pushr x))
     (fun a : A => ap e (pglue a))) (pglue a) @ 1 =
1 @ ap e (pglue a)
  apply equiv_p1_1q.
A, B, C: Type
f: A -> B
g: A -> C
P: Type
e: Pushout f g -> P
a: A
ap
  (Pushout_rec P (fun x : B => e (pushl x))
     (fun x : C => e (pushr x))
     (fun a : A => ap e (pglue a))) (pglue a) =
ap e (pglue a)
  nrapply Pushout_rec_beta_pglue.
Defined.

Definition isequiv_Pushout_rec `{Funext} {A B C} (f : A -> B) (g : A -> C) P
  : IsEquiv (fun p : {psh : (B -> P) * (C -> P) &
                            forall a, fst psh (f a) = snd psh (g a) }
             => Pushout_rec P (fst p.1) (snd p.1) p.2).
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
P: Type
IsEquiv
  (fun
     p : {psh : (B -> P) * (C -> P) &
         forall a : A, fst psh (f a) = snd psh (g a)}
   => Pushout_rec P (fst p.1) (snd p.1) p.2)
Proof.
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
P: Type
IsEquiv
  (fun
     p : {psh : (B -> P) * (C -> P) &
         forall a : A, fst psh (f a) = snd psh (g a)}
   => Pushout_rec P (fst p.1) (snd p.1) p.2)
  srefine (isequiv_adjointify _ (pushout_unrec f g) _ _).
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
P: Type
(fun
   p : {psh : (B -> P) * (C -> P) &
       forall a : A, fst psh (f a) = snd psh (g a)} =>
 Pushout_rec P (fst p.1) (snd p.1) p.2)
o pushout_unrec f g == idmap
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
P: Type
pushout_unrec f g
o (fun
     p : {psh : (B -> P) * (C -> P) &
         forall a : A, fst psh (f a) = snd psh (g a)}
   => Pushout_rec P (fst p.1) (snd p.1) p.2) == idmap
  -
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
P: Type
(fun
   p : {psh : (B -> P) * (C -> P) &
       forall a : A, fst psh (f a) = snd psh (g a)} =>
 Pushout_rec P (fst p.1) (snd p.1) p.2)
o pushout_unrec f g == idmap intro e.
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
P: Type
e: Pushout f g -> P
Pushout_rec P (fst (pushout_unrec f g e).1)
  (snd (pushout_unrec f g e).1)
  (pushout_unrec f g e).2 = e apply path_arrow.
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
P: Type
e: Pushout f g -> P
Pushout_rec P (fst (pushout_unrec f g e).1)
  (snd (pushout_unrec f g e).1)
  (pushout_unrec f g e).2 == e apply pushout_rec_unrec.
  -
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
P: Type
pushout_unrec f g
o (fun
     p : {psh : (B -> P) * (C -> P) &
         forall a : A, fst psh (f a) = snd psh (g a)}
   => Pushout_rec P (fst p.1) (snd p.1) p.2) == idmap intros [[pushb pushc] pusha]; unfold pushout_unrec; cbn.
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
P: Type
pushb: B -> P
pushc: C -> P
pusha: forall a : A,
fst (pushb, pushc) (f a) =
snd (pushb, pushc) (g a)
((fun x : B =>
  Pushout_rec P pushb pushc pusha (pushl x),
 fun x : C =>
 Pushout_rec P pushb pushc pusha (pushr x));
fun a : A =>
ap (Pushout_rec P pushb pushc pusha) (pglue a)) =
((pushb, pushc); pusha)
    snrapply path_sigma'.
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
P: Type
pushb: B -> P
pushc: C -> P
pusha: forall a : A,
fst (pushb, pushc) (f a) =
snd (pushb, pushc) (g a)
(fun x : B =>
 Pushout_rec P pushb pushc pusha (pushl x),
fun x : C => Pushout_rec P pushb pushc pusha (pushr x)) =
(pushb, pushc)
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
P: Type
pushb: B -> P
pushc: C -> P
pusha: forall a : A,
fst (pushb, pushc) (f a) =
snd (pushb, pushc) (g a)
transport
  (fun psh : (B -> P) * (C -> P) =>
   forall a : A, fst psh (f a) = snd psh (g a)) 
  ?p
  (fun a : A =>
   ap (Pushout_rec P pushb pushc pusha) (pglue a)) =
pusha
    +
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
P: Type
pushb: B -> P
pushc: C -> P
pusha: forall a : A,
fst (pushb, pushc) (f a) =
snd (pushb, pushc) (g a)
(fun x : B =>
 Pushout_rec P pushb pushc pusha (pushl x),
fun x : C => Pushout_rec P pushb pushc pusha (pushr x)) =
(pushb, pushc) reflexivity.
    +
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
P: Type
pushb: B -> P
pushc: C -> P
pusha: forall a : A,
fst (pushb, pushc) (f a) =
snd (pushb, pushc) (g a)
transport
  (fun psh : (B -> P) * (C -> P) =>
   forall a : A, fst psh (f a) = snd psh (g a)) 1
  (fun a : A =>
   ap (Pushout_rec P pushb pushc pusha) (pglue a)) =
pusha cbn.
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
P: Type
pushb: B -> P
pushc: C -> P
pusha: forall a : A,
fst (pushb, pushc) (f a) =
snd (pushb, pushc) (g a)
(fun a : A =>
 ap (Pushout_rec P pushb pushc pusha) (pglue a)) =
pusha apply path_forall; intros a.
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
P: Type
pushb: B -> P
pushc: C -> P
pusha: forall a : A,
fst (pushb, pushc) (f a) =
snd (pushb, pushc) (g a)
a: A
ap (Pushout_rec P pushb pushc pusha) (pglue a) =
pusha a
      apply Pushout_rec_beta_pglue.
Defined.

Definition equiv_Pushout_rec `{Funext} {A B C} (f : A -> B) (g : A -> C) P
  : {psh : (B -> P) * (C -> P) &
           forall a, fst psh (f a) = snd psh (g a) }
      <~> (Pushout f g -> P)
  := Build_Equiv _ _ _ (isequiv_Pushout_rec f g P).

Definition equiv_pushout_unrec `{Funext} {A B C} (f : A -> B) (g : A -> C) P
  : (Pushout f g -> P)
      <~> {psh : (B -> P) * (C -> P) &
                 forall a, fst psh (f a) = snd psh (g a) }
  := equiv_inverse (equiv_Pushout_rec f g P).

(** ** Symmetry *)

Definition pushout_sym_map {A B C} {f : A -> B} {g : A -> C}
  : Pushout f g -> Pushout g f
  := Pushout_rec (Pushout g f) pushr pushl (fun a : A => (pglue a)^).

Lemma sect_pushout_sym_map {A B C f g}
  : (@pushout_sym_map A B C f g) o (@pushout_sym_map A C B g f) == idmap.
A, B, C: Type
f: A -> B
g: A -> C
pushout_sym_map o pushout_sym_map == idmap
Proof.
A, B, C: Type
f: A -> B
g: A -> C
pushout_sym_map o pushout_sym_map == idmap
  srapply @Pushout_ind.
A, B, C: Type
f: A -> B
g: A -> C
forall b : C,
(fun w : Pushout g f =>
 (pushout_sym_map o pushout_sym_map) w = idmap w)
  (pushl b)
A, B, C: Type
f: A -> B
g: A -> C
forall c : B,
(fun w : Pushout g f =>
 (pushout_sym_map o pushout_sym_map) w = idmap w)
  (pushr c)
A, B, C: Type
f: A -> B
g: A -> C
forall a : A,
transport
  (fun w : Pushout g f =>
   (pushout_sym_map o pushout_sym_map) w = idmap w)
  (pglue a) (?pushb (g a)) = ?pushc (f a)
  -
A, B, C: Type
f: A -> B
g: A -> C
forall b : C,
(fun w : Pushout g f =>
 (pushout_sym_map o pushout_sym_map) w = idmap w)
  (pushl b) intros; reflexivity.
  -
A, B, C: Type
f: A -> B
g: A -> C
forall c : B,
(fun w : Pushout g f =>
 (pushout_sym_map o pushout_sym_map) w = idmap w)
  (pushr c) intros; reflexivity.
  -
A, B, C: Type
f: A -> B
g: A -> C
forall a : A,
transport
  (fun w : Pushout g f =>
   (pushout_sym_map o pushout_sym_map) w = idmap w)
  (pglue a) ((fun b : C => 1) (g a)) =
(fun c : B => 1) (f a) intro a.
A, B, C: Type
f: A -> B
g: A -> C
a: A
transport
  (fun w : Pushout g f =>
   (pushout_sym_map o pushout_sym_map) w = idmap w)
  (pglue a) ((fun b : C => 1) (g a)) =
(fun c : B => 1) (f a)
    simpl.
A, B, C: Type
f: A -> B
g: A -> C
a: A
transport
  (fun w : Pushout g f =>
   pushout_sym_map (pushout_sym_map w) = w) (pglue a)
  1 = 1
    abstract (rewrite transport_paths_FFlr, Pushout_rec_beta_pglue, ap_V, Pushout_rec_beta_pglue; hott_simpl).
Defined.

Definition pushout_sym {A B C} {f : A -> B} {g : A -> C}
  : Pushout f g <~> Pushout g f :=
equiv_adjointify pushout_sym_map pushout_sym_map sect_pushout_sym_map sect_pushout_sym_map.

(** ** Functoriality *)

Definition functor_pushout
  {A B C} {f : A -> B} {g : A -> C}
  {A' B' C'} {f' : A' -> B'} {g' : A' -> C'}
  (h : A -> A') (k : B -> B') (l : C -> C')
  (p : k o f == f' o h) (q : l o g == g' o h)
  : Pushout f g -> Pushout f' g'.
A, B, C: Type
f: A -> B
g: A -> C
A', B', C': Type
f': A' -> B'
g': A' -> C'
h: A -> A'
k: B -> B'
l: C -> C'
p: k o f == f' o h
q: l o g == g' o h
Pushout f g -> Pushout f' g'
Proof.
A, B, C: Type
f: A -> B
g: A -> C
A', B', C': Type
f': A' -> B'
g': A' -> C'
h: A -> A'
k: B -> B'
l: C -> C'
p: k o f == f' o h
q: l o g == g' o h
Pushout f g -> Pushout f' g'
  unfold Pushout; srapply functor_coeq.
A, B, C: Type
f: A -> B
g: A -> C
A', B', C': Type
f': A' -> B'
g': A' -> C'
h: A -> A'
k: B -> B'
l: C -> C'
p: k o f == f' o h
q: l o g == g' o h
A -> A'
A, B, C: Type
f: A -> B
g: A -> C
A', B', C': Type
f': A' -> B'
g': A' -> C'
h: A -> A'
k: B -> B'
l: C -> C'
p: k o f == f' o h
q: l o g == g' o h
B + C -> B' + C'
A, B, C: Type
f: A -> B
g: A -> C
A', B', C': Type
f': A' -> B'
g': A' -> C'
h: A -> A'
k: B -> B'
l: C -> C'
p: k o f == f' o h
q: l o g == g' o h
?k o (fun x : A => inl (f x)) ==
(fun x : A' => inl (f' x)) o ?h
A, B, C: Type
f: A -> B
g: A -> C
A', B', C': Type
f': A' -> B'
g': A' -> C'
h: A -> A'
k: B -> B'
l: C -> C'
p: k o f == f' o h
q: l o g == g' o h
?k o (fun x : A => inr (g x)) ==
(fun x : A' => inr (g' x)) o ?h
  -
A, B, C: Type
f: A -> B
g: A -> C
A', B', C': Type
f': A' -> B'
g': A' -> C'
h: A -> A'
k: B -> B'
l: C -> C'
p: k o f == f' o h
q: l o g == g' o h
A -> A' exact h.
  -
A, B, C: Type
f: A -> B
g: A -> C
A', B', C': Type
f': A' -> B'
g': A' -> C'
h: A -> A'
k: B -> B'
l: C -> C'
p: k o f == f' o h
q: l o g == g' o h
B + C -> B' + C' exact (functor_sum k l).
  -
A, B, C: Type
f: A -> B
g: A -> C
A', B', C': Type
f': A' -> B'
g': A' -> C'
h: A -> A'
k: B -> B'
l: C -> C'
p: k o f == f' o h
q: l o g == g' o h
functor_sum k l o (fun x : A => inl (f x)) ==
(fun x : A' => inl (f' x)) o h intros a; cbn.
A, B, C: Type
f: A -> B
g: A -> C
A', B', C': Type
f': A' -> B'
g': A' -> C'
h: A -> A'
k: B -> B'
l: C -> C'
p: k o f == f' o h
q: l o g == g' o h
a: A
inl (k (f a)) = inl (f' (h a))
    apply ap, p.
  -
A, B, C: Type
f: A -> B
g: A -> C
A', B', C': Type
f': A' -> B'
g': A' -> C'
h: A -> A'
k: B -> B'
l: C -> C'
p: k o f == f' o h
q: l o g == g' o h
functor_sum k l o (fun x : A => inr (g x)) ==
(fun x : A' => inr (g' x)) o h intros a; cbn.
A, B, C: Type
f: A -> B
g: A -> C
A', B', C': Type
f': A' -> B'
g': A' -> C'
h: A -> A'
k: B -> B'
l: C -> C'
p: k o f == f' o h
q: l o g == g' o h
a: A
inr (l (g a)) = inr (g' (h a))
    apply ap, q.
Defined.

Lemma functor_pushout_homotopic 
  {A B C : Type} {f : A -> B} {g : A -> C}
  {A' B' C' : Type} {f' : A' -> B'} {g' : A' -> C'}
  {h h' : A -> A'} {k k' : B -> B'} {l l' : C -> C'}
  {p : k o f == f' o h} {q : l o g == g' o h}
  {p' : k' o f == f' o h'} {q' : l' o g == g' o h'}
  (t : h == h') (u : k == k') (v : l == l')
  (i : forall a, p a @ (ap f') (t a) = u (f a) @ p' a)
  (j : forall a, q a @ (ap g') (t a) = v (g a) @ q' a)
  : functor_pushout h k l p q == functor_pushout h' k' l' p' q'.
A, B, C: Type
f: A -> B
g: A -> C
A', B', C': Type
f': A' -> B'
g': A' -> C'
h, h': A -> A'
k, k': B -> B'
l, l': C -> C'
p: k o f == f' o h
q: l o g == g' o h
p': k' o f == f' o h'
q': l' o g == g' o h'
t: h == h'
u: k == k'
v: l == l'
i: forall a : A, p a @ ap f' (t a) = u (f a) @ p' a
j: forall a : A, q a @ ap g' (t a) = v (g a) @ q' a
functor_pushout h k l p q ==
functor_pushout h' k' l' p' q'
Proof.
A, B, C: Type
f: A -> B
g: A -> C
A', B', C': Type
f': A' -> B'
g': A' -> C'
h, h': A -> A'
k, k': B -> B'
l, l': C -> C'
p: k o f == f' o h
q: l o g == g' o h
p': k' o f == f' o h'
q': l' o g == g' o h'
t: h == h'
u: k == k'
v: l == l'
i: forall a : A, p a @ ap f' (t a) = u (f a) @ p' a
j: forall a : A, q a @ ap g' (t a) = v (g a) @ q' a
functor_pushout h k l p q ==
functor_pushout h' k' l' p' q'
  srapply functor_coeq_homotopy.
A, B, C: Type
f: A -> B
g: A -> C
A', B', C': Type
f': A' -> B'
g': A' -> C'
h, h': A -> A'
k, k': B -> B'
l, l': C -> C'
p: k o f == f' o h
q: l o g == g' o h
p': k' o f == f' o h'
q': l' o g == g' o h'
t: h == h'
u: k == k'
v: l == l'
i: forall a : A, p a @ ap f' (t a) = u (f a) @ p' a
j: forall a : A, q a @ ap g' (t a) = v (g a) @ q' a
h == h'
A, B, C: Type
f: A -> B
g: A -> C
A', B', C': Type
f': A' -> B'
g': A' -> C'
h, h': A -> A'
k, k': B -> B'
l, l': C -> C'
p: k o f == f' o h
q: l o g == g' o h
p': k' o f == f' o h'
q': l' o g == g' o h'
t: h == h'
u: k == k'
v: l == l'
i: forall a : A, p a @ ap f' (t a) = u (f a) @ p' a
j: forall a : A, q a @ ap g' (t a) = v (g a) @ q' a
functor_sum k l == functor_sum k' l'
A, B, C: Type
f: A -> B
g: A -> C
A', B', C': Type
f': A' -> B'
g': A' -> C'
h, h': A -> A'
k, k': B -> B'
l, l': C -> C'
p: k o f == f' o h
q: l o g == g' o h
p': k' o f == f' o h'
q': l' o g == g' o h'
t: h == h'
u: k == k'
v: l == l'
i: forall a : A, p a @ ap f' (t a) = u (f a) @ p' a
j: forall a : A, q a @ ap g' (t a) = v (g a) @ q' a
forall b : A,
?s ((fun x : A => inl (f x)) b) @
(fun a : A =>
 ap inl (p' a)
 :
 functor_sum k' l' (inl (f a)) = inl (f' (h' a))) b =
(fun a : A =>
 ap inl (p a)
 :
 functor_sum k l (inl (f a)) = inl (f' (h a))) b @
ap (fun x : A' => inl (f' x)) (?r b)
A, B, C: Type
f: A -> B
g: A -> C
A', B', C': Type
f': A' -> B'
g': A' -> C'
h, h': A -> A'
k, k': B -> B'
l, l': C -> C'
p: k o f == f' o h
q: l o g == g' o h
p': k' o f == f' o h'
q': l' o g == g' o h'
t: h == h'
u: k == k'
v: l == l'
i: forall a : A, p a @ ap f' (t a) = u (f a) @ p' a
j: forall a : A, q a @ ap g' (t a) = v (g a) @ q' a
forall b : A,
?s ((fun x : A => inr (g x)) b) @
(fun a : A =>
 ap inr (q' a)
 :
 functor_sum k' l' (inr (g a)) = inr (g' (h' a))) b =
(fun a : A =>
 ap inr (q a)
 :
 functor_sum k l (inr (g a)) = inr (g' (h a))) b @
ap (fun x : A' => inr (g' x)) (?r b)
  1: exact t.
A, B, C: Type
f: A -> B
g: A -> C
A', B', C': Type
f': A' -> B'
g': A' -> C'
h, h': A -> A'
k, k': B -> B'
l, l': C -> C'
p: k o f == f' o h
q: l o g == g' o h
p': k' o f == f' o h'
q': l' o g == g' o h'
t: h == h'
u: k == k'
v: l == l'
i: forall a : A, p a @ ap f' (t a) = u (f a) @ p' a
j: forall a : A, q a @ ap g' (t a) = v (g a) @ q' a
functor_sum k l == functor_sum k' l'
A, B, C: Type
f: A -> B
g: A -> C
A', B', C': Type
f': A' -> B'
g': A' -> C'
h, h': A -> A'
k, k': B -> B'
l, l': C -> C'
p: k o f == f' o h
q: l o g == g' o h
p': k' o f == f' o h'
q': l' o g == g' o h'
t: h == h'
u: k == k'
v: l == l'
i: forall a : A, p a @ ap f' (t a) = u (f a) @ p' a
j: forall a : A, q a @ ap g' (t a) = v (g a) @ q' a
forall b : A,
?s ((fun x : A => inl (f x)) b) @
(fun a : A =>
 ap inl (p' a)
 :
 functor_sum k' l' (inl (f a)) = inl (f' (h' a))) b =
(fun a : A =>
 ap inl (p a)
 :
 functor_sum k l (inl (f a)) = inl (f' (h a))) b @
ap (fun x : A' => inl (f' x)) (t b)
A, B, C: Type
f: A -> B
g: A -> C
A', B', C': Type
f': A' -> B'
g': A' -> C'
h, h': A -> A'
k, k': B -> B'
l, l': C -> C'
p: k o f == f' o h
q: l o g == g' o h
p': k' o f == f' o h'
q': l' o g == g' o h'
t: h == h'
u: k == k'
v: l == l'
i: forall a : A, p a @ ap f' (t a) = u (f a) @ p' a
j: forall a : A, q a @ ap g' (t a) = v (g a) @ q' a
forall b : A,
?s ((fun x : A => inr (g x)) b) @
(fun a : A =>
 ap inr (q' a)
 :
 functor_sum k' l' (inr (g a)) = inr (g' (h' a))) b =
(fun a : A =>
 ap inr (q a)
 :
 functor_sum k l (inr (g a)) = inr (g' (h a))) b @
ap (fun x : A' => inr (g' x)) (t b)
  1: exact (functor_sum_homotopic u v).
A, B, C: Type
f: A -> B
g: A -> C
A', B', C': Type
f': A' -> B'
g': A' -> C'
h, h': A -> A'
k, k': B -> B'
l, l': C -> C'
p: k o f == f' o h
q: l o g == g' o h
p': k' o f == f' o h'
q': l' o g == g' o h'
t: h == h'
u: k == k'
v: l == l'
i: forall a : A, p a @ ap f' (t a) = u (f a) @ p' a
j: forall a : A, q a @ ap g' (t a) = v (g a) @ q' a
forall b : A,
functor_sum_homotopic u v ((fun x : A => inl (f x)) b) @
(fun a : A =>
 ap inl (p' a)
 :
 functor_sum k' l' (inl (f a)) = inl (f' (h' a))) b =
(fun a : A =>
 ap inl (p a)
 :
 functor_sum k l (inl (f a)) = inl (f' (h a))) b @
ap (fun x : A' => inl (f' x)) (t b)
A, B, C: Type
f: A -> B
g: A -> C
A', B', C': Type
f': A' -> B'
g': A' -> C'
h, h': A -> A'
k, k': B -> B'
l, l': C -> C'
p: k o f == f' o h
q: l o g == g' o h
p': k' o f == f' o h'
q': l' o g == g' o h'
t: h == h'
u: k == k'
v: l == l'
i: forall a : A, p a @ ap f' (t a) = u (f a) @ p' a
j: forall a : A, q a @ ap g' (t a) = v (g a) @ q' a
forall b : A,
functor_sum_homotopic u v ((fun x : A => inr (g x)) b) @
(fun a : A =>
 ap inr (q' a)
 :
 functor_sum k' l' (inr (g a)) = inr (g' (h' a))) b =
(fun a : A =>
 ap inr (q a)
 :
 functor_sum k l (inr (g a)) = inr (g' (h a))) b @
ap (fun x : A' => inr (g' x)) (t b)
  1,2: intros b; simpl.
A, B, C: Type
f: A -> B
g: A -> C
A', B', C': Type
f': A' -> B'
g': A' -> C'
h, h': A -> A'
k, k': B -> B'
l, l': C -> C'
p: k o f == f' o h
q: l o g == g' o h
p': k' o f == f' o h'
q': l' o g == g' o h'
t: h == h'
u: k == k'
v: l == l'
i: forall a : A, p a @ ap f' (t a) = u (f a) @ p' a
j: forall a : A, q a @ ap g' (t a) = v (g a) @ q' a
b: A
ap inl (u (f b)) @ ap inl (p' b) =
ap inl (p b) @ ap (fun x : A' => inl (f' x)) (t b)
A, B, C: Type
f: A -> B
g: A -> C
A', B', C': Type
f': A' -> B'
g': A' -> C'
h, h': A -> A'
k, k': B -> B'
l, l': C -> C'
p: k o f == f' o h
q: l o g == g' o h
p': k' o f == f' o h'
q': l' o g == g' o h'
t: h == h'
u: k == k'
v: l == l'
i: forall a : A, p a @ ap f' (t a) = u (f a) @ p' a
j: forall a : A, q a @ ap g' (t a) = v (g a) @ q' a
b: A
ap inr (v (g b)) @ ap inr (q' b) =
ap inr (q b) @ ap (fun x : A' => inr (g' x)) (t b)
  1,2: refine (_ @ ap_pp _ _ _ @ ap _ (ap_compose _ _ _)^).
A, B, C: Type
f: A -> B
g: A -> C
A', B', C': Type
f': A' -> B'
g': A' -> C'
h, h': A -> A'
k, k': B -> B'
l, l': C -> C'
p: k o f == f' o h
q: l o g == g' o h
p': k' o f == f' o h'
q': l' o g == g' o h'
t: h == h'
u: k == k'
v: l == l'
i: forall a : A, p a @ ap f' (t a) = u (f a) @ p' a
j: forall a : A, q a @ ap g' (t a) = v (g a) @ q' a
b: A
ap inl (u (f b)) @ ap inl (p' b) =
ap inl (p b @ ap f' (t b))
A, B, C: Type
f: A -> B
g: A -> C
A', B', C': Type
f': A' -> B'
g': A' -> C'
h, h': A -> A'
k, k': B -> B'
l, l': C -> C'
p: k o f == f' o h
q: l o g == g' o h
p': k' o f == f' o h'
q': l' o g == g' o h'
t: h == h'
u: k == k'
v: l == l'
i: forall a : A, p a @ ap f' (t a) = u (f a) @ p' a
j: forall a : A, q a @ ap g' (t a) = v (g a) @ q' a
b: A
ap inr (v (g b)) @ ap inr (q' b) =
ap inr (q b @ ap g' (t b))
  1,2: refine ((ap_pp _ _ _)^ @ ap _ _^).
A, B, C: Type
f: A -> B
g: A -> C
A', B', C': Type
f': A' -> B'
g': A' -> C'
h, h': A -> A'
k, k': B -> B'
l, l': C -> C'
p: k o f == f' o h
q: l o g == g' o h
p': k' o f == f' o h'
q': l' o g == g' o h'
t: h == h'
u: k == k'
v: l == l'
i: forall a : A, p a @ ap f' (t a) = u (f a) @ p' a
j: forall a : A, q a @ ap g' (t a) = v (g a) @ q' a
b: A
p b @ ap f' (t b) = u (f b) @ p' b
A, B, C: Type
f: A -> B
g: A -> C
A', B', C': Type
f': A' -> B'
g': A' -> C'
h, h': A -> A'
k, k': B -> B'
l, l': C -> C'
p: k o f == f' o h
q: l o g == g' o h
p': k' o f == f' o h'
q': l' o g == g' o h'
t: h == h'
u: k == k'
v: l == l'
i: forall a : A, p a @ ap f' (t a) = u (f a) @ p' a
j: forall a : A, q a @ ap g' (t a) = v (g a) @ q' a
b: A
q b @ ap g' (t b) = v (g b) @ q' b
  1: exact (i b).
A, B, C: Type
f: A -> B
g: A -> C
A', B', C': Type
f': A' -> B'
g': A' -> C'
h, h': A -> A'
k, k': B -> B'
l, l': C -> C'
p: k o f == f' o h
q: l o g == g' o h
p': k' o f == f' o h'
q': l' o g == g' o h'
t: h == h'
u: k == k'
v: l == l'
i: forall a : A, p a @ ap f' (t a) = u (f a) @ p' a
j: forall a : A, q a @ ap g' (t a) = v (g a) @ q' a
b: A
q b @ ap g' (t b) = v (g b) @ q' b
  exact (j b).
Defined.


(** ** Equivalences *)

(** Pushouts preserve equivalences. *)

Section EquivPushout.
  Context {A B C f g A' B' C' f' g'}
          (eA : A <~> A') (eB : B <~> B') (eC : C <~> C')
          (p : eB o f == f' o eA) (q : eC o g == g' o eA).

  Lemma equiv_pushout
    : Pushout f g <~> Pushout f' g'.
A, B, C: Type
f: A -> B
g: A -> C
A', B', C': Type
f': A' -> B'
g': A' -> C'
eA: A <~> A'
eB: B <~> B'
eC: C <~> C'
p: eB o f == f' o eA
q: eC o g == g' o eA
Pushout f g <~> Pushout f' g'
  Proof.
A, B, C: Type
f: A -> B
g: A -> C
A', B', C': Type
f': A' -> B'
g': A' -> C'
eA: A <~> A'
eB: B <~> B'
eC: C <~> C'
p: eB o f == f' o eA
q: eC o g == g' o eA
Pushout f g <~> Pushout f' g'
    refine (equiv_functor_coeq' eA (equiv_functor_sum' eB eC) _ _).
A, B, C: Type
f: A -> B
g: A -> C
A', B', C': Type
f': A' -> B'
g': A' -> C'
eA: A <~> A'
eB: B <~> B'
eC: C <~> C'
p: eB o f == f' o eA
q: eC o g == g' o eA
(fun x : A => (eB +E eC) (inl (f x))) ==
(fun x : A => inl (f' (eA x)))
A, B, C: Type
f: A -> B
g: A -> C
A', B', C': Type
f': A' -> B'
g': A' -> C'
eA: A <~> A'
eB: B <~> B'
eC: C <~> C'
p: eB o f == f' o eA
q: eC o g == g' o eA
(fun x : A => (eB +E eC) (inr (g x))) ==
(fun x : A => inr (g' (eA x)))
    all:unfold pointwise_paths.
A, B, C: Type
f: A -> B
g: A -> C
A', B', C': Type
f': A' -> B'
g': A' -> C'
eA: A <~> A'
eB: B <~> B'
eC: C <~> C'
p: eB o f == f' o eA
q: eC o g == g' o eA
forall x : A, (eB +E eC) (inl (f x)) = inl (f' (eA x))
A, B, C: Type
f: A -> B
g: A -> C
A', B', C': Type
f': A' -> B'
g': A' -> C'
eA: A <~> A'
eB: B <~> B'
eC: C <~> C'
p: eB o f == f' o eA
q: eC o g == g' o eA
forall x : A, (eB +E eC) (inr (g x)) = inr (g' (eA x))
    all:intro; simpl; apply ap.
A, B, C: Type
f: A -> B
g: A -> C
A', B', C': Type
f': A' -> B'
g': A' -> C'
eA: A <~> A'
eB: B <~> B'
eC: C <~> C'
p: eB o f == f' o eA
q: eC o g == g' o eA
x: A
eB (f x) = f' (eA x)
A, B, C: Type
f: A -> B
g: A -> C
A', B', C': Type
f': A' -> B'
g': A' -> C'
eA: A <~> A'
eB: B <~> B'
eC: C <~> C'
p: eB o f == f' o eA
q: eC o g == g' o eA
x: A
eC (g x) = g' (eA x)
    +
A, B, C: Type
f: A -> B
g: A -> C
A', B', C': Type
f': A' -> B'
g': A' -> C'
eA: A <~> A'
eB: B <~> B'
eC: C <~> C'
p: eB o f == f' o eA
q: eC o g == g' o eA
x: A
eB (f x) = f' (eA x) apply p.
    +
A, B, C: Type
f: A -> B
g: A -> C
A', B', C': Type
f': A' -> B'
g': A' -> C'
eA: A <~> A'
eB: B <~> B'
eC: C <~> C'
p: eB o f == f' o eA
q: eC o g == g' o eA
x: A
eC (g x) = g' (eA x) apply q.
  Defined.

  Lemma equiv_pushout_pglue (a : A)
    : ap equiv_pushout (pglue a)
      = ap pushl (p a) @ pglue (eA a) @ ap pushr (q a)^.
A, B, C: Type
f: A -> B
g: A -> C
A', B', C': Type
f': A' -> B'
g': A' -> C'
eA: A <~> A'
eB: B <~> B'
eC: C <~> C'
p: eB o f == f' o eA
q: eC o g == g' o eA
a: A
ap equiv_pushout (pglue a) =
(ap pushl (p a) @ pglue (eA a)) @ ap pushr (q a)^
  Proof.
A, B, C: Type
f: A -> B
g: A -> C
A', B', C': Type
f': A' -> B'
g': A' -> C'
eA: A <~> A'
eB: B <~> B'
eC: C <~> C'
p: eB o f == f' o eA
q: eC o g == g' o eA
a: A
ap equiv_pushout (pglue a) =
(ap pushl (p a) @ pglue (eA a)) @ ap pushr (q a)^
    refine (functor_coeq_beta_cglue _ _ _ _ a @ _).
A, B, C: Type
f: A -> B
g: A -> C
A', B', C': Type
f': A' -> B'
g': A' -> C'
eA: A <~> A'
eB: B <~> B'
eC: C <~> C'
p: eB o f == f' o eA
q: eC o g == g' o eA
a: A
(ap coeq (ap inl (p a)) @ cglue (eA a)) @
ap coeq (ap inr (q a))^ =
(ap pushl (p a) @ pglue (eA a)) @ ap pushr (q a)^
    refine (_ @@ 1 @@ _).
A, B, C: Type
f: A -> B
g: A -> C
A', B', C': Type
f': A' -> B'
g': A' -> C'
eA: A <~> A'
eB: B <~> B'
eC: C <~> C'
p: eB o f == f' o eA
q: eC o g == g' o eA
a: A
ap coeq (ap inl (p a)) = ap pushl (p a)
A, B, C: Type
f: A -> B
g: A -> C
A', B', C': Type
f': A' -> B'
g': A' -> C'
eA: A <~> A'
eB: B <~> B'
eC: C <~> C'
p: eB o f == f' o eA
q: eC o g == g' o eA
a: A
ap coeq (ap inr (q a))^ = ap pushr (q a)^
    -
A, B, C: Type
f: A -> B
g: A -> C
A', B', C': Type
f': A' -> B'
g': A' -> C'
eA: A <~> A'
eB: B <~> B'
eC: C <~> C'
p: eB o f == f' o eA
q: eC o g == g' o eA
a: A
ap coeq (ap inl (p a)) = ap pushl (p a) symmetry; refine (ap_compose inl coeq _).
    -
A, B, C: Type
f: A -> B
g: A -> C
A', B', C': Type
f': A' -> B'
g': A' -> C'
eA: A <~> A'
eB: B <~> B'
eC: C <~> C'
p: eB o f == f' o eA
q: eC o g == g' o eA
a: A
ap coeq (ap inr (q a))^ = ap pushr (q a)^ refine (ap (ap coeq) (ap_V _ _)^ @ _).
A, B, C: Type
f: A -> B
g: A -> C
A', B', C': Type
f': A' -> B'
g': A' -> C'
eA: A <~> A'
eB: B <~> B'
eC: C <~> C'
p: eB o f == f' o eA
q: eC o g == g' o eA
a: A
ap coeq (ap inr (q a)^) = ap pushr (q a)^
      symmetry; refine (ap_compose inr coeq _).
  Defined.

End EquivPushout.

(** ** Contractibility *)

(** The pushout of a span of contractible types is contractible *)

Global Instance contr_pushout {A B C : Type} `{Contr A, Contr B, Contr C}
       (f : A -> B) (g : A -> C)
  : Contr (Pushout f g).
A, B, C: Type
Contr0: Contr A
Contr1: Contr B
Contr2: Contr C
f: A -> B
g: A -> C
Contr (Pushout f g)
Proof.
A, B, C: Type
Contr0: Contr A
Contr1: Contr B
Contr2: Contr C
f: A -> B
g: A -> C
Contr (Pushout f g)
  apply (Build_Contr _ (pushl (center B))).
A, B, C: Type
Contr0: Contr A
Contr1: Contr B
Contr2: Contr C
f: A -> B
g: A -> C
forall y : Pushout f g, pushl (center B) = y
  srapply Pushout_ind.
A, B, C: Type
Contr0: Contr A
Contr1: Contr B
Contr2: Contr C
f: A -> B
g: A -> C
forall b : B, pushl (center B) = pushl b
A, B, C: Type
Contr0: Contr A
Contr1: Contr B
Contr2: Contr C
f: A -> B
g: A -> C
forall c : C, pushl (center B) = pushr c
A, B, C: Type
Contr0: Contr A
Contr1: Contr B
Contr2: Contr C
f: A -> B
g: A -> C
forall a : A,
transport (paths (pushl (center B))) 
  (pglue a) (?pushb (f a)) = 
?pushc (g a)
  -
A, B, C: Type
Contr0: Contr A
Contr1: Contr B
Contr2: Contr C
f: A -> B
g: A -> C
forall b : B, pushl (center B) = pushl b intros b; apply ap, path_contr.
  -
A, B, C: Type
Contr0: Contr A
Contr1: Contr B
Contr2: Contr C
f: A -> B
g: A -> C
forall c : C, pushl (center B) = pushr c intros c.
A, B, C: Type
Contr0: Contr A
Contr1: Contr B
Contr2: Contr C
f: A -> B
g: A -> C
c: C
pushl (center B) = pushr c
    refine (_ @ pglue (center A) @ _).
A, B, C: Type
Contr0: Contr A
Contr1: Contr B
Contr2: Contr C
f: A -> B
g: A -> C
c: C
pushl (center B) = pushl (f (center A))
A, B, C: Type
Contr0: Contr A
Contr1: Contr B
Contr2: Contr C
f: A -> B
g: A -> C
c: C
pushr (g (center A)) = pushr c
    +
A, B, C: Type
Contr0: Contr A
Contr1: Contr B
Contr2: Contr C
f: A -> B
g: A -> C
c: C
pushl (center B) = pushl (f (center A)) apply ap, path_contr.
    +
A, B, C: Type
Contr0: Contr A
Contr1: Contr B
Contr2: Contr C
f: A -> B
g: A -> C
c: C
pushr (g (center A)) = pushr c apply ap, path_contr.
  -
A, B, C: Type
Contr0: Contr A
Contr1: Contr B
Contr2: Contr C
f: A -> B
g: A -> C
forall a : A,
transport (paths (pushl (center B))) (pglue a)
  ((fun b : B => ap pushl (path_contr (center B) b))
     (f a)) =
(fun c : C =>
 (ap pushl (path_contr (center B) (f (center A))) @
  pglue (center A)) @
 ap pushr (path_contr (g (center A)) c)) (g a) intros a.
A, B, C: Type
Contr0: Contr A
Contr1: Contr B
Contr2: Contr C
f: A -> B
g: A -> C
a: A
transport (paths (pushl (center B))) (pglue a)
  ((fun b : B => ap pushl (path_contr (center B) b))
     (f a)) =
(fun c : C =>
 (ap pushl (path_contr (center B) (f (center A))) @
  pglue (center A)) @
 ap pushr (path_contr (g (center A)) c)) (g a)
    rewrite transport_paths_r.
A, B, C: Type
Contr0: Contr A
Contr1: Contr B
Contr2: Contr C
f: A -> B
g: A -> C
a: A
ap pushl (path_contr (center B) (f a)) @ pglue a =
(ap pushl (path_contr (center B) (f (center A))) @
 pglue (center A)) @
ap pushr (path_contr (g (center A)) (g a))
    assert (p := path_contr (center A) a).
A, B, C: Type
Contr0: Contr A
Contr1: Contr B
Contr2: Contr C
f: A -> B
g: A -> C
a: A
p: center A = a
ap pushl (path_contr (center B) (f a)) @ pglue a =
(ap pushl (path_contr (center B) (f (center A))) @
 pglue (center A)) @
ap pushr (path_contr (g (center A)) (g a))
    destruct p.
A, B, C: Type
Contr0: Contr A
Contr1: Contr B
Contr2: Contr C
f: A -> B
g: A -> C
ap pushl (path_contr (center B) (f (center A))) @
pglue (center A) =
(ap pushl (path_contr (center B) (f (center A))) @
 pglue (center A)) @
ap pushr (path_contr (g (center A)) (g (center A)))
    refine ((concat_p1 _)^ @ _).
A, B, C: Type
Contr0: Contr A
Contr1: Contr B
Contr2: Contr C
f: A -> B
g: A -> C
(ap pushl (path_contr (center B) (f (center A))) @
 pglue (center A)) @ 1 =
(ap pushl (path_contr (center B) (f (center A))) @
 pglue (center A)) @
ap pushr (path_contr (g (center A)) (g (center A)))
    apply whiskerL.
A, B, C: Type
Contr0: Contr A
Contr1: Contr B
Contr2: Contr C
f: A -> B
g: A -> C
1 =
ap pushr (path_contr (g (center A)) (g (center A)))
    change 1 with (ap (@pushr A B C f g) (idpath (g (center A)))).
A, B, C: Type
Contr0: Contr A
Contr1: Contr B
Contr2: Contr C
f: A -> B
g: A -> C
ap pushr 1 =
ap pushr (path_contr (g (center A)) (g (center A)))
    apply (ap (ap pushr)).
A, B, C: Type
Contr0: Contr A
Contr1: Contr B
Contr2: Contr C
f: A -> B
g: A -> C
1 = path_contr (g (center A)) (g (center A))
    apply path_contr.
Defined.

(** ** Sigmas *)

(** Pushouts commute with sigmas *)

Section EquivSigmaPushout.

  Context {X : Type}
          (A : X -> Type) (B : X -> Type) (C : X -> Type)
          (f : forall x, A x -> B x) (g : forall x, A x -> C x).

  Local Definition esp1 : { x : X & Pushout (f x) (g x) }
             -> Pushout (functor_sigma idmap f) (functor_sigma idmap g).
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
{x : X & Pushout (f x) (g x)} ->
Pushout (functor_sigma idmap f)
  (functor_sigma idmap g)
  Proof.
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
{x : X & Pushout (f x) (g x)} ->
Pushout (functor_sigma idmap f)
  (functor_sigma idmap g)
    intros [x p].
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
x: X
p: Pushout (f x) (g x)
Pushout (functor_sigma idmap f)
  (functor_sigma idmap g)
    srefine (Pushout_rec _ _ _ _ p).
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
x: X
p: Pushout (f x) (g x)
B x ->
Pushout (functor_sigma idmap f)
  (functor_sigma idmap g)
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
x: X
p: Pushout (f x) (g x)
C x ->
Pushout (functor_sigma idmap f)
  (functor_sigma idmap g)
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
x: X
p: Pushout (f x) (g x)
forall a : A x, ?pushb (f x a) = ?pushc (g x a)
    +
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
x: X
p: Pushout (f x) (g x)
B x ->
Pushout (functor_sigma idmap f)
  (functor_sigma idmap g) intros b.
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
x: X
p: Pushout (f x) (g x)
b: B x
Pushout (functor_sigma idmap f)
  (functor_sigma idmap g) exact (pushl (x;b)).
    +
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
x: X
p: Pushout (f x) (g x)
C x ->
Pushout (functor_sigma idmap f)
  (functor_sigma idmap g) intros c.
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
x: X
p: Pushout (f x) (g x)
c: C x
Pushout (functor_sigma idmap f)
  (functor_sigma idmap g) exact (pushr (x;c)).
    +
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
x: X
p: Pushout (f x) (g x)
forall a : A x,
(fun b : B x => pushl (x; b)) (f x a) =
(fun c : C x => pushr (x; c)) (g x a) intros a; cbn.
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
x: X
p: Pushout (f x) (g x)
a: A x
pushl (x; f x a) = pushr (x; g x a) exact (pglue (x;a)).
  Defined.

  Local Definition esp1_beta_pglue (x : X) (a : A x)
    : ap esp1 (path_sigma' (fun x => Pushout (f x) (g x)) 1 (pglue a))
      = pglue (x;a).
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
x: X
a: A x
ap esp1
  (path_sigma' (fun x : X => Pushout (f x) (g x)) 1
     (pglue a)) = pglue (x; a)
  Proof.
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
x: X
a: A x
ap esp1
  (path_sigma' (fun x : X => Pushout (f x) (g x)) 1
     (pglue a)) = pglue (x; a)
    rewrite (ap_path_sigma (fun x => Pushout (f x) (g x))
                           (fun x a => esp1 (x;a)) 1 (pglue a)); cbn.
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
x: X
a: A x
(ap (fun a : Pushout (f x) (g x) => esp1 (x; a))
   (pglue a) @ 1) @ 1 = pglue (x; a)
    rewrite !concat_p1.
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
x: X
a: A x
ap (fun a : Pushout (f x) (g x) => esp1 (x; a))
  (pglue a) = pglue (x; a)
    unfold esp1; rewrite Pushout_rec_beta_pglue.
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
x: X
a: A x
pglue (x; a) = pglue (x; a)
    reflexivity.
  Qed.

  Local Definition esp2 : Pushout (functor_sigma idmap f) (functor_sigma idmap g)
             -> { x : X & Pushout (f x) (g x) }.
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
Pushout (functor_sigma idmap f)
  (functor_sigma idmap g) ->
{x : X & Pushout (f x) (g x)}
  Proof.
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
Pushout (functor_sigma idmap f)
  (functor_sigma idmap g) ->
{x : X & Pushout (f x) (g x)}
    srefine (Pushout_rec _ _ _ _).
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
{x : _ & B x} -> {x : X & Pushout (f x) (g x)}
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
{x : _ & C x} -> {x : X & Pushout (f x) (g x)}
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
forall a : {x : _ & A x},
?pushb (functor_sigma idmap f a) =
?pushc (functor_sigma idmap g a)
    +
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
{x : _ & B x} -> {x : X & Pushout (f x) (g x)} exact (functor_sigma idmap (fun x => @pushl _ _ _ (f x) (g x))).
    +
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
{x : _ & C x} -> {x : X & Pushout (f x) (g x)} exact (functor_sigma idmap (fun x => @pushr _ _ _ (f x) (g x))).
    +
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
forall a : {x : _ & A x},
functor_sigma idmap (fun x : X => pushl)
  (functor_sigma idmap f a) =
functor_sigma idmap (fun x : X => pushr)
  (functor_sigma idmap g a) intros [x a]; unfold functor_sigma; cbn.
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
x: X
a: A x
(x; pushl (f x a)) = (x; pushr (g x a))
      srefine (path_sigma' _ 1 _); cbn.
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
x: X
a: A x
pushl (f x a) = pushr (g x a)
      apply pglue.
  Defined.

  Local Definition esp2_beta_pglue (x : X) (a : A x)
    : ap esp2 (pglue (x;a)) = path_sigma' (fun x:X => Pushout (f x) (g x)) 1 (pglue a).
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
x: X
a: A x
ap esp2 (pglue (x; a)) =
path_sigma' (fun x : X => Pushout (f x) (g x)) 1
  (pglue a)
  Proof.
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
x: X
a: A x
ap esp2 (pglue (x; a)) =
path_sigma' (fun x : X => Pushout (f x) (g x)) 1
  (pglue a)
    unfold esp2.
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
x: X
a: A x
ap
  (Pushout_rec {x : X & Pushout (f x) (g x)}
     (functor_sigma idmap (fun x : X => pushl))
     (functor_sigma idmap (fun x : X => pushr))
     (fun a0 : {x : _ & A x} =>
      path_sigma' (fun x : X => Pushout (f x) (g x)) 1
        (pglue a0.2))) (pglue (x; a)) =
path_sigma' (fun x : X => Pushout (f x) (g x)) 1
  (pglue a)
    rewrite Pushout_rec_beta_pglue.
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
x: X
a: A x
path_sigma' (fun x : X => Pushout (f x) (g x)) 1
  (pglue a) =
path_sigma' (fun x : X => Pushout (f x) (g x)) 1
  (pglue a)
    reflexivity.
  Qed.

  Definition equiv_sigma_pushout
    : { x : X & Pushout (f x) (g x) }
        <~> Pushout (functor_sigma idmap f) (functor_sigma idmap g).
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
{x : X & Pushout (f x) (g x)} <~>
Pushout (functor_sigma idmap f)
  (functor_sigma idmap g)
  Proof.
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
{x : X & Pushout (f x) (g x)} <~>
Pushout (functor_sigma idmap f)
  (functor_sigma idmap g)
    srefine (equiv_adjointify esp1 esp2 _ _).
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
esp1 o esp2 == idmap
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
esp2 o esp1 == idmap
    -
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
esp1 o esp2 == idmap srefine (Pushout_ind _ _ _ _); cbn.
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
forall b : {x : _ & B x},
esp1 (esp2 (pushl b)) = pushl b
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
forall c : {x : _ & C x},
esp1 (esp2 (pushr c)) = pushr c
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
forall a : {x : _ & A x},
transport
  (fun
     w : Pushout (functor_sigma idmap f)
           (functor_sigma idmap g) =>
   esp1 (esp2 w) = w) (pglue a)
  (?Goal (functor_sigma idmap f a)) =
?Goal0 (functor_sigma idmap g a)
      +
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
forall b : {x : _ & B x},
esp1 (esp2 (pushl b)) = pushl b reflexivity.
      +
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
forall c : {x : _ & C x},
esp1 (esp2 (pushr c)) = pushr c reflexivity.
      +
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
forall a : {x : _ & A x},
transport
  (fun
     w : Pushout (functor_sigma idmap f)
           (functor_sigma idmap g) =>
   esp1 (esp2 w) = w) (pglue a)
  ((fun b : {x : _ & B x} => 1)
     (functor_sigma idmap f a)) =
(fun c : {x : _ & C x} => 1) (functor_sigma idmap g a) intros [x a].
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
x: X
a: A x
transport
  (fun
     w : Pushout (functor_sigma idmap f)
           (functor_sigma idmap g) =>
   esp1 (esp2 w) = w) (pglue (x; a)) 1 = 1
        refine (transport_paths_FFlr _ _ @ _).
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
x: X
a: A x
((ap esp1 (ap esp2 (pglue (x; a))))^ @ 1) @
pglue (x; a) = 1
        refine (concat_p1 _ @@ 1 @ _).
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
x: X
a: A x
(ap esp1 (ap esp2 (pglue (x; a))))^ @ pglue (x; a) = 1
        apply moveR_Vp; symmetry.
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
x: X
a: A x
ap esp1 (ap esp2 (pglue (x; a))) @ 1 = pglue (x; a)
        refine (concat_p1 _ @ _).
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
x: X
a: A x
ap esp1 (ap esp2 (pglue (x; a))) = pglue (x; a)
        refine (ap _ (esp2_beta_pglue _ _) @ _).
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
x: X
a: A x
ap esp1
  (path_sigma' (fun x : X => Pushout (f x) (g x)) 1
     (pglue a)) = pglue (x; a)
        apply esp1_beta_pglue.
    -
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
esp2 o esp1 == idmap intros [x a]; revert a.
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
x: X
forall a : Pushout (f x) (g x),
esp2 (esp1 (x; a)) = (x; a)
      srefine (Pushout_ind _ _ _ _); cbn.
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
x: X
forall b : B x,
esp2 (esp1 (x; pushl b)) = (x; pushl b)
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
x: X
forall c : C x,
esp2 (esp1 (x; pushr c)) = (x; pushr c)
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
x: X
forall a : A x,
transport
  (fun w : Pushout (f x) (g x) =>
   esp2 (esp1 (x; w)) = (x; w)) (pglue a)
  (?Goal (f x a)) = ?Goal0 (g x a)
      +
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
x: X
forall b : B x,
esp2 (esp1 (x; pushl b)) = (x; pushl b) reflexivity.
      +
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
x: X
forall c : C x,
esp2 (esp1 (x; pushr c)) = (x; pushr c) reflexivity.
      +
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
x: X
forall a : A x,
transport
  (fun w : Pushout (f x) (g x) =>
   esp2 (esp1 (x; w)) = (x; w)) (pglue a)
  ((fun b : B x => 1) (f x a)) =
(fun c : C x => 1) (g x a) intros a.
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
x: X
a: A x
transport
  (fun w : Pushout (f x) (g x) =>
   esp2 (esp1 (x; w)) = (x; w)) (pglue a)
  ((fun b : B x => 1) (f x a)) =
(fun c : C x => 1) (g x a)
        rewrite transport_paths_FlFr.
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
x: X
a: A x
((ap
    (fun x0 : Pushout (f x) (g x) =>
     esp2 (esp1 (x; x0))) (pglue a))^ @ 1) @
ap (exist (fun x : X => Pushout (f x) (g x)) x)
  (pglue a) = 1
        rewrite concat_p1; apply moveR_Vp; rewrite concat_p1.
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
x: X
a: A x
ap (exist (fun x : X => Pushout (f x) (g x)) x)
  (pglue a) =
ap
  (fun x0 : Pushout (f x) (g x) => esp2 (esp1 (x; x0)))
  (pglue a)
        rewrite (ap_compose (exist _ x) (esp2 o esp1)).
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
x: X
a: A x
ap (exist (fun x : X => Pushout (f x) (g x)) x)
  (pglue a) =
ap
  (fun x : {x : X & Pushout (f x) (g x)} =>
   esp2 (esp1 x))
  (ap (exist (fun x : X => Pushout (f x) (g x)) x)
     (pglue a))
        rewrite (ap_compose esp1 esp2).
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
x: X
a: A x
ap (exist (fun x : X => Pushout (f x) (g x)) x)
  (pglue a) =
ap esp2
  (ap esp1
     (ap (exist (fun x : X => Pushout (f x) (g x)) x)
        (pglue a)))
        rewrite (ap_exist (fun x => Pushout (f x) (g x)) x _ _ (pglue a)).
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
x: X
a: A x
path_sigma' (fun x : X => Pushout (f x) (g x)) 1
  (pglue a) =
ap esp2
  (ap esp1
     (path_sigma' (fun x : X => Pushout (f x) (g x)) 1
        (pglue a)))
        rewrite esp1_beta_pglue, esp2_beta_pglue.
X: Type
A, B, C: X -> Type
f: forall x : X, A x -> B x
g: forall x : X, A x -> C x
x: X
a: A x
path_sigma' (fun x : X => Pushout (f x) (g x)) 1
  (pglue a) =
path_sigma' (fun x : X => Pushout (f x) (g x)) 1
  (pglue a)
        reflexivity.
  Defined.

End EquivSigmaPushout.

(** ** Pushouts are associative *)

Section PushoutAssoc.

  Context {A1 A2 B C D : Type}
          (f1 : A1 -> B) (g1 : A1 -> C) (f2 : A2 -> C) (g2 : A2 -> D).

  Definition pushout_assoc_left := Pushout (pushr' f1 g1 o f2) g2.
  Let pushll : B -> pushout_assoc_left
    := pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1.
  Let pushlm : C -> pushout_assoc_left
    := pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1.
  Let pushlr : D -> pushout_assoc_left
    := pushr' (pushr' f1 g1 o f2) g2.
  Let pgluell : forall a1, pushll (f1 a1) = pushlm (g1 a1)
    := fun a1 => ap (pushl' (pushr' f1 g1 o f2) g2) (pglue' f1 g1 a1).
  Let pgluelr : forall a2, pushlm (f2 a2) = pushlr (g2 a2)
    := fun a2 => pglue' (pushr' f1 g1 o f2) g2 a2.

  Definition pushout_assoc_left_ind
             (P : pushout_assoc_left -> Type)
             (pushb : forall b, P (pushll b))
             (pushc : forall c, P (pushlm c))
             (pushd : forall d, P (pushlr d))
             (pusha1 : forall a1, (pgluell a1) # pushb (f1 a1) = pushc (g1 a1))
             (pusha2 : forall a2, (pgluelr a2) # pushc (f2 a2) = pushd (g2 a2))
    : forall x, P x.
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
P: pushout_assoc_left -> Type
pushb: forall b : B, P (pushll b)
pushc: forall c : C, P (pushlm c)
pushd: forall d : D, P (pushlr d)
pusha1: forall a1 : A1,
transport P (pgluell a1) (pushb (f1 a1)) =
pushc (g1 a1)
pusha2: forall a2 : A2,
transport P (pgluelr a2) (pushc (f2 a2)) =
pushd (g2 a2)
forall x : pushout_assoc_left, P x
  Proof.
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
P: pushout_assoc_left -> Type
pushb: forall b : B, P (pushll b)
pushc: forall c : C, P (pushlm c)
pushd: forall d : D, P (pushlr d)
pusha1: forall a1 : A1,
transport P (pgluell a1) (pushb (f1 a1)) =
pushc (g1 a1)
pusha2: forall a2 : A2,
transport P (pgluelr a2) (pushc (f2 a2)) =
pushd (g2 a2)
forall x : pushout_assoc_left, P x
    srefine (Pushout_ind _ _ pushd _).
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
P: pushout_assoc_left -> Type
pushb: forall b : B, P (pushll b)
pushc: forall c : C, P (pushlm c)
pushd: forall d : D, P (pushlr d)
pusha1: forall a1 : A1,
transport P (pgluell a1) (pushb (f1 a1)) =
pushc (g1 a1)
pusha2: forall a2 : A2,
transport P (pgluelr a2) (pushc (f2 a2)) =
pushd (g2 a2)
forall b : Pushout f1 g1, P (pushl b)
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
P: pushout_assoc_left -> Type
pushb: forall b : B, P (pushll b)
pushc: forall c : C, P (pushlm c)
pushd: forall d : D, P (pushlr d)
pusha1: forall a1 : A1,
transport P (pgluell a1) (pushb (f1 a1)) =
pushc (g1 a1)
pusha2: forall a2 : A2,
transport P (pgluelr a2) (pushc (f2 a2)) =
pushd (g2 a2)
forall a : A2,
transport P (pglue a)
  (?pushb ((fun x : A2 => pushr' f1 g1 (f2 x)) a)) =
pushd (g2 a)
    -
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
P: pushout_assoc_left -> Type
pushb: forall b : B, P (pushll b)
pushc: forall c : C, P (pushlm c)
pushd: forall d : D, P (pushlr d)
pusha1: forall a1 : A1,
transport P (pgluell a1) (pushb (f1 a1)) =
pushc (g1 a1)
pusha2: forall a2 : A2,
transport P (pgluelr a2) (pushc (f2 a2)) =
pushd (g2 a2)
forall b : Pushout f1 g1, P (pushl b) srefine (Pushout_ind _ pushb pushc _).
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
P: pushout_assoc_left -> Type
pushb: forall b : B, P (pushll b)
pushc: forall c : C, P (pushlm c)
pushd: forall d : D, P (pushlr d)
pusha1: forall a1 : A1,
transport P (pgluell a1) (pushb (f1 a1)) =
pushc (g1 a1)
pusha2: forall a2 : A2,
transport P (pgluelr a2) (pushc (f2 a2)) =
pushd (g2 a2)
forall a : A1,
transport (fun w : Pushout f1 g1 => P (pushl w))
  (pglue a) (pushb (f1 a)) = pushc (g1 a)
      intros a1.
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
P: pushout_assoc_left -> Type
pushb: forall b : B, P (pushll b)
pushc: forall c : C, P (pushlm c)
pushd: forall d : D, P (pushlr d)
pusha1: forall a1 : A1,
transport P (pgluell a1) (pushb (f1 a1)) =
pushc (g1 a1)
pusha2: forall a2 : A2,
transport P (pgluelr a2) (pushc (f2 a2)) =
pushd (g2 a2)
a1: A1
transport (fun w : Pushout f1 g1 => P (pushl w))
  (pglue a1) (pushb (f1 a1)) = pushc (g1 a1)
      exact (transport_compose P pushl _ _ @ pusha1 a1).
    -
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
P: pushout_assoc_left -> Type
pushb: forall b : B, P (pushll b)
pushc: forall c : C, P (pushlm c)
pushd: forall d : D, P (pushlr d)
pusha1: forall a1 : A1,
transport P (pgluell a1) (pushb (f1 a1)) =
pushc (g1 a1)
pusha2: forall a2 : A2,
transport P (pgluelr a2) (pushc (f2 a2)) =
pushd (g2 a2)
forall a : A2,
transport P (pglue a)
  (Pushout_ind (fun w : Pushout f1 g1 => P (pushl w))
     pushb pushc
     (fun a1 : A1 =>
      transport_compose P pushl (pglue' f1 g1 a1)
        (pushb (f1 a1)) @ pusha1 a1)
     ((fun x : A2 => pushr' f1 g1 (f2 x)) a)) =
pushd (g2 a) exact pusha2.
  Defined.

  Section Pushout_Assoc_Left_Rec.

    Context (P : Type)
            (pushb : B -> P)
            (pushc : C -> P)
            (pushd : D -> P)
            (pusha1 : forall a1, pushb (f1 a1) = pushc (g1 a1))
            (pusha2 : forall a2, pushc (f2 a2) = pushd (g2 a2)).

    Definition pushout_assoc_left_rec
      : pushout_assoc_left -> P.
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
P: Type
pushb: B -> P
pushc: C -> P
pushd: D -> P
pusha1: forall a1 : A1, pushb (f1 a1) = pushc (g1 a1)
pusha2: forall a2 : A2, pushc (f2 a2) = pushd (g2 a2)
pushout_assoc_left -> P
    Proof.
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
P: Type
pushb: B -> P
pushc: C -> P
pushd: D -> P
pusha1: forall a1 : A1, pushb (f1 a1) = pushc (g1 a1)
pusha2: forall a2 : A2, pushc (f2 a2) = pushd (g2 a2)
pushout_assoc_left -> P
      srefine (Pushout_rec _ _ pushd _).
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
P: Type
pushb: B -> P
pushc: C -> P
pushd: D -> P
pusha1: forall a1 : A1, pushb (f1 a1) = pushc (g1 a1)
pusha2: forall a2 : A2, pushc (f2 a2) = pushd (g2 a2)
Pushout f1 g1 -> P
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
P: Type
pushb: B -> P
pushc: C -> P
pushd: D -> P
pusha1: forall a1 : A1, pushb (f1 a1) = pushc (g1 a1)
pusha2: forall a2 : A2, pushc (f2 a2) = pushd (g2 a2)
forall a : A2,
?pushb ((fun x : A2 => pushr' f1 g1 (f2 x)) a) =
pushd (g2 a)
      -
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
P: Type
pushb: B -> P
pushc: C -> P
pushd: D -> P
pusha1: forall a1 : A1, pushb (f1 a1) = pushc (g1 a1)
pusha2: forall a2 : A2, pushc (f2 a2) = pushd (g2 a2)
Pushout f1 g1 -> P srefine (Pushout_rec _ pushb pushc pusha1).
      -
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
P: Type
pushb: B -> P
pushc: C -> P
pushd: D -> P
pusha1: forall a1 : A1, pushb (f1 a1) = pushc (g1 a1)
pusha2: forall a2 : A2, pushc (f2 a2) = pushd (g2 a2)
forall a : A2,
Pushout_rec P pushb pushc pusha1
  ((fun x : A2 => pushr' f1 g1 (f2 x)) a) =
pushd (g2 a) exact pusha2.
    Defined.

    Definition pushout_assoc_left_rec_beta_pgluell a1
      : ap pushout_assoc_left_rec (pgluell a1) = pusha1 a1.
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
P: Type
pushb: B -> P
pushc: C -> P
pushd: D -> P
pusha1: forall a1 : A1, pushb (f1 a1) = pushc (g1 a1)
pusha2: forall a2 : A2, pushc (f2 a2) = pushd (g2 a2)
a1: A1
ap pushout_assoc_left_rec (pgluell a1) = pusha1 a1
    Proof.
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
P: Type
pushb: B -> P
pushc: C -> P
pushd: D -> P
pusha1: forall a1 : A1, pushb (f1 a1) = pushc (g1 a1)
pusha2: forall a2 : A2, pushc (f2 a2) = pushd (g2 a2)
a1: A1
ap pushout_assoc_left_rec (pgluell a1) = pusha1 a1
      unfold pgluell.
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
P: Type
pushb: B -> P
pushc: C -> P
pushd: D -> P
pusha1: forall a1 : A1, pushb (f1 a1) = pushc (g1 a1)
pusha2: forall a2 : A2, pushc (f2 a2) = pushd (g2 a2)
a1: A1
ap pushout_assoc_left_rec
  (ap (pushl' (fun x : A2 => pushr' f1 g1 (f2 x)) g2)
     (pglue' f1 g1 a1)) = pusha1 a1
      rewrite <- (ap_compose (pushl' (pushr' f1 g1 o f2) g2)
                             pushout_assoc_left_rec).
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
P: Type
pushb: B -> P
pushc: C -> P
pushd: D -> P
pusha1: forall a1 : A1, pushb (f1 a1) = pushc (g1 a1)
pusha2: forall a2 : A2, pushc (f2 a2) = pushd (g2 a2)
a1: A1
ap
  (fun x : Pushout f1 g1 =>
   pushout_assoc_left_rec
     (pushl' (fun x0 : A2 => pushr' f1 g1 (f2 x0)) g2
        x)) (pglue' f1 g1 a1) = pusha1 a1
      change (ap (Pushout_rec P pushb pushc pusha1) (pglue' f1 g1 a1) = pusha1 a1).
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
P: Type
pushb: B -> P
pushc: C -> P
pushd: D -> P
pusha1: forall a1 : A1, pushb (f1 a1) = pushc (g1 a1)
pusha2: forall a2 : A2, pushc (f2 a2) = pushd (g2 a2)
a1: A1
ap (Pushout_rec P pushb pushc pusha1)
  (pglue' f1 g1 a1) = pusha1 a1
      apply Pushout_rec_beta_pglue.
    Defined.

    Definition pushout_assoc_left_rec_beta_pgluelr a2
      : ap pushout_assoc_left_rec (pgluelr a2) = pusha2 a2.
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
P: Type
pushb: B -> P
pushc: C -> P
pushd: D -> P
pusha1: forall a1 : A1, pushb (f1 a1) = pushc (g1 a1)
pusha2: forall a2 : A2, pushc (f2 a2) = pushd (g2 a2)
a2: A2
ap pushout_assoc_left_rec (pgluelr a2) = pusha2 a2
    Proof.
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
P: Type
pushb: B -> P
pushc: C -> P
pushd: D -> P
pusha1: forall a1 : A1, pushb (f1 a1) = pushc (g1 a1)
pusha2: forall a2 : A2, pushc (f2 a2) = pushd (g2 a2)
a2: A2
ap pushout_assoc_left_rec (pgluelr a2) = pusha2 a2
      unfold pushout_assoc_left_rec, pgluelr.
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
P: Type
pushb: B -> P
pushc: C -> P
pushd: D -> P
pusha1: forall a1 : A1, pushb (f1 a1) = pushc (g1 a1)
pusha2: forall a2 : A2, pushc (f2 a2) = pushd (g2 a2)
a2: A2
ap
  (Pushout_rec P (Pushout_rec P pushb pushc pusha1)
     pushd pusha2)
  (pglue' (fun x : A2 => pushr' f1 g1 (f2 x)) g2 a2) =
pusha2 a2
      apply (Pushout_rec_beta_pglue (f := pushr' f1 g1 o f2) (g := g2)).
    Defined.

  End Pushout_Assoc_Left_Rec.

  Definition pushout_assoc_right := Pushout f1 (pushl' f2 g2 o g1).
  Let pushrl : B -> pushout_assoc_right
    := pushl' f1 (pushl' f2 g2 o g1).
  Let pushrm : C -> pushout_assoc_right
    := pushr' f1 (pushl' f2 g2 o g1) o pushl' f2 g2.
  Let pushrr : D -> pushout_assoc_right
    := pushr' f1 (pushl' f2 g2 o g1) o pushr' f2 g2.
  Let pgluerl : forall a1, pushrl (f1 a1) = pushrm (g1 a1)
    := fun a1 => pglue' f1 (pushl' f2 g2 o g1) a1.
  Let pgluerr : forall a2, pushrm (f2 a2) = pushrr (g2 a2)
    := fun a2 => ap (pushr' f1 (pushl' f2 g2 o g1)) (pglue' f2 g2 a2).

  Definition pushout_assoc_right_ind
             (P : pushout_assoc_right -> Type)
             (pushb : forall b, P (pushrl b))
             (pushc : forall c, P (pushrm c))
             (pushd : forall d, P (pushrr d))
             (pusha1 : forall a1, (pgluerl a1) # pushb (f1 a1) = pushc (g1 a1))
             (pusha2 : forall a2, (pgluerr a2) # pushc (f2 a2) = pushd (g2 a2))
    : forall x, P x.
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
pushrl:= pushl' f1 (pushl' f2 g2 o g1): B -> pushout_assoc_right
pushrm:= pushr' f1 (pushl' f2 g2 o g1) o pushl' f2 g2: C -> pushout_assoc_right
pushrr:= pushr' f1 (pushl' f2 g2 o g1) o pushr' f2 g2: D -> pushout_assoc_right
pgluerl:= fun a1 : A1 =>
pglue' f1 (pushl' f2 g2 o g1) a1: forall a1 : A1,
pushrl (f1 a1) = pushrm (g1 a1)
pgluerr:= fun a2 : A2 =>
ap (pushr' f1 (pushl' f2 g2 o g1))
  (pglue' f2 g2 a2): forall a2 : A2,
pushrm (f2 a2) = pushrr (g2 a2)
P: pushout_assoc_right -> Type
pushb: forall b : B, P (pushrl b)
pushc: forall c : C, P (pushrm c)
pushd: forall d : D, P (pushrr d)
pusha1: forall a1 : A1,
transport P (pgluerl a1) (pushb (f1 a1)) =
pushc (g1 a1)
pusha2: forall a2 : A2,
transport P (pgluerr a2) (pushc (f2 a2)) =
pushd (g2 a2)
forall x : pushout_assoc_right, P x
  Proof.
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
pushrl:= pushl' f1 (pushl' f2 g2 o g1): B -> pushout_assoc_right
pushrm:= pushr' f1 (pushl' f2 g2 o g1) o pushl' f2 g2: C -> pushout_assoc_right
pushrr:= pushr' f1 (pushl' f2 g2 o g1) o pushr' f2 g2: D -> pushout_assoc_right
pgluerl:= fun a1 : A1 =>
pglue' f1 (pushl' f2 g2 o g1) a1: forall a1 : A1,
pushrl (f1 a1) = pushrm (g1 a1)
pgluerr:= fun a2 : A2 =>
ap (pushr' f1 (pushl' f2 g2 o g1))
  (pglue' f2 g2 a2): forall a2 : A2,
pushrm (f2 a2) = pushrr (g2 a2)
P: pushout_assoc_right -> Type
pushb: forall b : B, P (pushrl b)
pushc: forall c : C, P (pushrm c)
pushd: forall d : D, P (pushrr d)
pusha1: forall a1 : A1,
transport P (pgluerl a1) (pushb (f1 a1)) =
pushc (g1 a1)
pusha2: forall a2 : A2,
transport P (pgluerr a2) (pushc (f2 a2)) =
pushd (g2 a2)
forall x : pushout_assoc_right, P x
    srefine (Pushout_ind _ pushb _ _).
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
pushrl:= pushl' f1 (pushl' f2 g2 o g1): B -> pushout_assoc_right
pushrm:= pushr' f1 (pushl' f2 g2 o g1) o pushl' f2 g2: C -> pushout_assoc_right
pushrr:= pushr' f1 (pushl' f2 g2 o g1) o pushr' f2 g2: D -> pushout_assoc_right
pgluerl:= fun a1 : A1 =>
pglue' f1 (pushl' f2 g2 o g1) a1: forall a1 : A1,
pushrl (f1 a1) = pushrm (g1 a1)
pgluerr:= fun a2 : A2 =>
ap (pushr' f1 (pushl' f2 g2 o g1))
  (pglue' f2 g2 a2): forall a2 : A2,
pushrm (f2 a2) = pushrr (g2 a2)
P: pushout_assoc_right -> Type
pushb: forall b : B, P (pushrl b)
pushc: forall c : C, P (pushrm c)
pushd: forall d : D, P (pushrr d)
pusha1: forall a1 : A1,
transport P (pgluerl a1) (pushb (f1 a1)) =
pushc (g1 a1)
pusha2: forall a2 : A2,
transport P (pgluerr a2) (pushc (f2 a2)) =
pushd (g2 a2)
forall c : Pushout f2 g2, P (pushr c)
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
pushrl:= pushl' f1 (pushl' f2 g2 o g1): B -> pushout_assoc_right
pushrm:= pushr' f1 (pushl' f2 g2 o g1) o pushl' f2 g2: C -> pushout_assoc_right
pushrr:= pushr' f1 (pushl' f2 g2 o g1) o pushr' f2 g2: D -> pushout_assoc_right
pgluerl:= fun a1 : A1 =>
pglue' f1 (pushl' f2 g2 o g1) a1: forall a1 : A1,
pushrl (f1 a1) = pushrm (g1 a1)
pgluerr:= fun a2 : A2 =>
ap (pushr' f1 (pushl' f2 g2 o g1))
  (pglue' f2 g2 a2): forall a2 : A2,
pushrm (f2 a2) = pushrr (g2 a2)
P: pushout_assoc_right -> Type
pushb: forall b : B, P (pushrl b)
pushc: forall c : C, P (pushrm c)
pushd: forall d : D, P (pushrr d)
pusha1: forall a1 : A1,
transport P (pgluerl a1) (pushb (f1 a1)) =
pushc (g1 a1)
pusha2: forall a2 : A2,
transport P (pgluerr a2) (pushc (f2 a2)) =
pushd (g2 a2)
forall a : A1,
transport P (pglue a) (pushb (f1 a)) =
?pushc ((fun x : A1 => pushl' f2 g2 (g1 x)) a)
    -
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
pushrl:= pushl' f1 (pushl' f2 g2 o g1): B -> pushout_assoc_right
pushrm:= pushr' f1 (pushl' f2 g2 o g1) o pushl' f2 g2: C -> pushout_assoc_right
pushrr:= pushr' f1 (pushl' f2 g2 o g1) o pushr' f2 g2: D -> pushout_assoc_right
pgluerl:= fun a1 : A1 =>
pglue' f1 (pushl' f2 g2 o g1) a1: forall a1 : A1,
pushrl (f1 a1) = pushrm (g1 a1)
pgluerr:= fun a2 : A2 =>
ap (pushr' f1 (pushl' f2 g2 o g1))
  (pglue' f2 g2 a2): forall a2 : A2,
pushrm (f2 a2) = pushrr (g2 a2)
P: pushout_assoc_right -> Type
pushb: forall b : B, P (pushrl b)
pushc: forall c : C, P (pushrm c)
pushd: forall d : D, P (pushrr d)
pusha1: forall a1 : A1,
transport P (pgluerl a1) (pushb (f1 a1)) =
pushc (g1 a1)
pusha2: forall a2 : A2,
transport P (pgluerr a2) (pushc (f2 a2)) =
pushd (g2 a2)
forall c : Pushout f2 g2, P (pushr c) srefine (Pushout_ind _ pushc pushd _).
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
pushrl:= pushl' f1 (pushl' f2 g2 o g1): B -> pushout_assoc_right
pushrm:= pushr' f1 (pushl' f2 g2 o g1) o pushl' f2 g2: C -> pushout_assoc_right
pushrr:= pushr' f1 (pushl' f2 g2 o g1) o pushr' f2 g2: D -> pushout_assoc_right
pgluerl:= fun a1 : A1 =>
pglue' f1 (pushl' f2 g2 o g1) a1: forall a1 : A1,
pushrl (f1 a1) = pushrm (g1 a1)
pgluerr:= fun a2 : A2 =>
ap (pushr' f1 (pushl' f2 g2 o g1))
  (pglue' f2 g2 a2): forall a2 : A2,
pushrm (f2 a2) = pushrr (g2 a2)
P: pushout_assoc_right -> Type
pushb: forall b : B, P (pushrl b)
pushc: forall c : C, P (pushrm c)
pushd: forall d : D, P (pushrr d)
pusha1: forall a1 : A1,
transport P (pgluerl a1) (pushb (f1 a1)) =
pushc (g1 a1)
pusha2: forall a2 : A2,
transport P (pgluerr a2) (pushc (f2 a2)) =
pushd (g2 a2)
forall a : A2,
transport (fun w : Pushout f2 g2 => P (pushr w))
  (pglue a) (pushc (f2 a)) = pushd (g2 a)
      intros a2.
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
pushrl:= pushl' f1 (pushl' f2 g2 o g1): B -> pushout_assoc_right
pushrm:= pushr' f1 (pushl' f2 g2 o g1) o pushl' f2 g2: C -> pushout_assoc_right
pushrr:= pushr' f1 (pushl' f2 g2 o g1) o pushr' f2 g2: D -> pushout_assoc_right
pgluerl:= fun a1 : A1 =>
pglue' f1 (pushl' f2 g2 o g1) a1: forall a1 : A1,
pushrl (f1 a1) = pushrm (g1 a1)
pgluerr:= fun a2 : A2 =>
ap (pushr' f1 (pushl' f2 g2 o g1))
  (pglue' f2 g2 a2): forall a2 : A2,
pushrm (f2 a2) = pushrr (g2 a2)
P: pushout_assoc_right -> Type
pushb: forall b : B, P (pushrl b)
pushc: forall c : C, P (pushrm c)
pushd: forall d : D, P (pushrr d)
pusha1: forall a1 : A1,
transport P (pgluerl a1) (pushb (f1 a1)) =
pushc (g1 a1)
pusha2: forall a2 : A2,
transport P (pgluerr a2) (pushc (f2 a2)) =
pushd (g2 a2)
a2: A2
transport (fun w : Pushout f2 g2 => P (pushr w))
  (pglue a2) (pushc (f2 a2)) = pushd (g2 a2)
      exact (transport_compose P pushr _ _ @ pusha2 a2).
    -
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
pushrl:= pushl' f1 (pushl' f2 g2 o g1): B -> pushout_assoc_right
pushrm:= pushr' f1 (pushl' f2 g2 o g1) o pushl' f2 g2: C -> pushout_assoc_right
pushrr:= pushr' f1 (pushl' f2 g2 o g1) o pushr' f2 g2: D -> pushout_assoc_right
pgluerl:= fun a1 : A1 =>
pglue' f1 (pushl' f2 g2 o g1) a1: forall a1 : A1,
pushrl (f1 a1) = pushrm (g1 a1)
pgluerr:= fun a2 : A2 =>
ap (pushr' f1 (pushl' f2 g2 o g1))
  (pglue' f2 g2 a2): forall a2 : A2,
pushrm (f2 a2) = pushrr (g2 a2)
P: pushout_assoc_right -> Type
pushb: forall b : B, P (pushrl b)
pushc: forall c : C, P (pushrm c)
pushd: forall d : D, P (pushrr d)
pusha1: forall a1 : A1,
transport P (pgluerl a1) (pushb (f1 a1)) =
pushc (g1 a1)
pusha2: forall a2 : A2,
transport P (pgluerr a2) (pushc (f2 a2)) =
pushd (g2 a2)
forall a : A1,
transport P (pglue a) (pushb (f1 a)) =
Pushout_ind (fun w : Pushout f2 g2 => P (pushr w))
  pushc pushd
  (fun a2 : A2 =>
   transport_compose P pushr (pglue' f2 g2 a2)
     (pushc (f2 a2)) @ pusha2 a2)
  ((fun x : A1 => pushl' f2 g2 (g1 x)) a) exact pusha1.
  Defined.

  Section Pushout_Assoc_Right_Rec.

    Context (P : Type)
            (pushb : B -> P)
            (pushc : C -> P)
            (pushd : D -> P)
            (pusha1 : forall a1, pushb (f1 a1) = pushc (g1 a1))
            (pusha2 : forall a2, pushc (f2 a2) = pushd (g2 a2)).

    Definition pushout_assoc_right_rec
      : pushout_assoc_right -> P.
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
pushrl:= pushl' f1 (pushl' f2 g2 o g1): B -> pushout_assoc_right
pushrm:= pushr' f1 (pushl' f2 g2 o g1) o pushl' f2 g2: C -> pushout_assoc_right
pushrr:= pushr' f1 (pushl' f2 g2 o g1) o pushr' f2 g2: D -> pushout_assoc_right
pgluerl:= fun a1 : A1 =>
pglue' f1 (pushl' f2 g2 o g1) a1: forall a1 : A1,
pushrl (f1 a1) = pushrm (g1 a1)
pgluerr:= fun a2 : A2 =>
ap (pushr' f1 (pushl' f2 g2 o g1))
  (pglue' f2 g2 a2): forall a2 : A2,
pushrm (f2 a2) = pushrr (g2 a2)
P: Type
pushb: B -> P
pushc: C -> P
pushd: D -> P
pusha1: forall a1 : A1, pushb (f1 a1) = pushc (g1 a1)
pusha2: forall a2 : A2, pushc (f2 a2) = pushd (g2 a2)
pushout_assoc_right -> P
    Proof.
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
pushrl:= pushl' f1 (pushl' f2 g2 o g1): B -> pushout_assoc_right
pushrm:= pushr' f1 (pushl' f2 g2 o g1) o pushl' f2 g2: C -> pushout_assoc_right
pushrr:= pushr' f1 (pushl' f2 g2 o g1) o pushr' f2 g2: D -> pushout_assoc_right
pgluerl:= fun a1 : A1 =>
pglue' f1 (pushl' f2 g2 o g1) a1: forall a1 : A1,
pushrl (f1 a1) = pushrm (g1 a1)
pgluerr:= fun a2 : A2 =>
ap (pushr' f1 (pushl' f2 g2 o g1))
  (pglue' f2 g2 a2): forall a2 : A2,
pushrm (f2 a2) = pushrr (g2 a2)
P: Type
pushb: B -> P
pushc: C -> P
pushd: D -> P
pusha1: forall a1 : A1, pushb (f1 a1) = pushc (g1 a1)
pusha2: forall a2 : A2, pushc (f2 a2) = pushd (g2 a2)
pushout_assoc_right -> P
      srefine (Pushout_rec _ pushb _ _).
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
pushrl:= pushl' f1 (pushl' f2 g2 o g1): B -> pushout_assoc_right
pushrm:= pushr' f1 (pushl' f2 g2 o g1) o pushl' f2 g2: C -> pushout_assoc_right
pushrr:= pushr' f1 (pushl' f2 g2 o g1) o pushr' f2 g2: D -> pushout_assoc_right
pgluerl:= fun a1 : A1 =>
pglue' f1 (pushl' f2 g2 o g1) a1: forall a1 : A1,
pushrl (f1 a1) = pushrm (g1 a1)
pgluerr:= fun a2 : A2 =>
ap (pushr' f1 (pushl' f2 g2 o g1))
  (pglue' f2 g2 a2): forall a2 : A2,
pushrm (f2 a2) = pushrr (g2 a2)
P: Type
pushb: B -> P
pushc: C -> P
pushd: D -> P
pusha1: forall a1 : A1, pushb (f1 a1) = pushc (g1 a1)
pusha2: forall a2 : A2, pushc (f2 a2) = pushd (g2 a2)
Pushout f2 g2 -> P
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
pushrl:= pushl' f1 (pushl' f2 g2 o g1): B -> pushout_assoc_right
pushrm:= pushr' f1 (pushl' f2 g2 o g1) o pushl' f2 g2: C -> pushout_assoc_right
pushrr:= pushr' f1 (pushl' f2 g2 o g1) o pushr' f2 g2: D -> pushout_assoc_right
pgluerl:= fun a1 : A1 =>
pglue' f1 (pushl' f2 g2 o g1) a1: forall a1 : A1,
pushrl (f1 a1) = pushrm (g1 a1)
pgluerr:= fun a2 : A2 =>
ap (pushr' f1 (pushl' f2 g2 o g1))
  (pglue' f2 g2 a2): forall a2 : A2,
pushrm (f2 a2) = pushrr (g2 a2)
P: Type
pushb: B -> P
pushc: C -> P
pushd: D -> P
pusha1: forall a1 : A1, pushb (f1 a1) = pushc (g1 a1)
pusha2: forall a2 : A2, pushc (f2 a2) = pushd (g2 a2)
forall a : A1,
pushb (f1 a) =
?pushc ((fun x : A1 => pushl' f2 g2 (g1 x)) a)
      -
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
pushrl:= pushl' f1 (pushl' f2 g2 o g1): B -> pushout_assoc_right
pushrm:= pushr' f1 (pushl' f2 g2 o g1) o pushl' f2 g2: C -> pushout_assoc_right
pushrr:= pushr' f1 (pushl' f2 g2 o g1) o pushr' f2 g2: D -> pushout_assoc_right
pgluerl:= fun a1 : A1 =>
pglue' f1 (pushl' f2 g2 o g1) a1: forall a1 : A1,
pushrl (f1 a1) = pushrm (g1 a1)
pgluerr:= fun a2 : A2 =>
ap (pushr' f1 (pushl' f2 g2 o g1))
  (pglue' f2 g2 a2): forall a2 : A2,
pushrm (f2 a2) = pushrr (g2 a2)
P: Type
pushb: B -> P
pushc: C -> P
pushd: D -> P
pusha1: forall a1 : A1, pushb (f1 a1) = pushc (g1 a1)
pusha2: forall a2 : A2, pushc (f2 a2) = pushd (g2 a2)
Pushout f2 g2 -> P srefine (Pushout_rec _ pushc pushd pusha2).
      -
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
pushrl:= pushl' f1 (pushl' f2 g2 o g1): B -> pushout_assoc_right
pushrm:= pushr' f1 (pushl' f2 g2 o g1) o pushl' f2 g2: C -> pushout_assoc_right
pushrr:= pushr' f1 (pushl' f2 g2 o g1) o pushr' f2 g2: D -> pushout_assoc_right
pgluerl:= fun a1 : A1 =>
pglue' f1 (pushl' f2 g2 o g1) a1: forall a1 : A1,
pushrl (f1 a1) = pushrm (g1 a1)
pgluerr:= fun a2 : A2 =>
ap (pushr' f1 (pushl' f2 g2 o g1))
  (pglue' f2 g2 a2): forall a2 : A2,
pushrm (f2 a2) = pushrr (g2 a2)
P: Type
pushb: B -> P
pushc: C -> P
pushd: D -> P
pusha1: forall a1 : A1, pushb (f1 a1) = pushc (g1 a1)
pusha2: forall a2 : A2, pushc (f2 a2) = pushd (g2 a2)
forall a : A1,
pushb (f1 a) =
Pushout_rec P pushc pushd pusha2
  ((fun x : A1 => pushl' f2 g2 (g1 x)) a) exact pusha1.
    Defined.

    Definition pushout_assoc_right_rec_beta_pgluerl a1
      : ap pushout_assoc_right_rec (pgluerl a1) = pusha1 a1.
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
pushrl:= pushl' f1 (pushl' f2 g2 o g1): B -> pushout_assoc_right
pushrm:= pushr' f1 (pushl' f2 g2 o g1) o pushl' f2 g2: C -> pushout_assoc_right
pushrr:= pushr' f1 (pushl' f2 g2 o g1) o pushr' f2 g2: D -> pushout_assoc_right
pgluerl:= fun a1 : A1 =>
pglue' f1 (pushl' f2 g2 o g1) a1: forall a1 : A1,
pushrl (f1 a1) = pushrm (g1 a1)
pgluerr:= fun a2 : A2 =>
ap (pushr' f1 (pushl' f2 g2 o g1))
  (pglue' f2 g2 a2): forall a2 : A2,
pushrm (f2 a2) = pushrr (g2 a2)
P: Type
pushb: B -> P
pushc: C -> P
pushd: D -> P
pusha1: forall a1 : A1, pushb (f1 a1) = pushc (g1 a1)
pusha2: forall a2 : A2, pushc (f2 a2) = pushd (g2 a2)
a1: A1
ap pushout_assoc_right_rec (pgluerl a1) = pusha1 a1
    Proof.
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
pushrl:= pushl' f1 (pushl' f2 g2 o g1): B -> pushout_assoc_right
pushrm:= pushr' f1 (pushl' f2 g2 o g1) o pushl' f2 g2: C -> pushout_assoc_right
pushrr:= pushr' f1 (pushl' f2 g2 o g1) o pushr' f2 g2: D -> pushout_assoc_right
pgluerl:= fun a1 : A1 =>
pglue' f1 (pushl' f2 g2 o g1) a1: forall a1 : A1,
pushrl (f1 a1) = pushrm (g1 a1)
pgluerr:= fun a2 : A2 =>
ap (pushr' f1 (pushl' f2 g2 o g1))
  (pglue' f2 g2 a2): forall a2 : A2,
pushrm (f2 a2) = pushrr (g2 a2)
P: Type
pushb: B -> P
pushc: C -> P
pushd: D -> P
pusha1: forall a1 : A1, pushb (f1 a1) = pushc (g1 a1)
pusha2: forall a2 : A2, pushc (f2 a2) = pushd (g2 a2)
a1: A1
ap pushout_assoc_right_rec (pgluerl a1) = pusha1 a1
      unfold pushout_assoc_right_rec, pgluerl.
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
pushrl:= pushl' f1 (pushl' f2 g2 o g1): B -> pushout_assoc_right
pushrm:= pushr' f1 (pushl' f2 g2 o g1) o pushl' f2 g2: C -> pushout_assoc_right
pushrr:= pushr' f1 (pushl' f2 g2 o g1) o pushr' f2 g2: D -> pushout_assoc_right
pgluerl:= fun a1 : A1 =>
pglue' f1 (pushl' f2 g2 o g1) a1: forall a1 : A1,
pushrl (f1 a1) = pushrm (g1 a1)
pgluerr:= fun a2 : A2 =>
ap (pushr' f1 (pushl' f2 g2 o g1))
  (pglue' f2 g2 a2): forall a2 : A2,
pushrm (f2 a2) = pushrr (g2 a2)
P: Type
pushb: B -> P
pushc: C -> P
pushd: D -> P
pusha1: forall a1 : A1, pushb (f1 a1) = pushc (g1 a1)
pusha2: forall a2 : A2, pushc (f2 a2) = pushd (g2 a2)
a1: A1
ap
  (Pushout_rec P pushb
     (Pushout_rec P pushc pushd pusha2) pusha1)
  (pglue' f1 (fun x : A1 => pushl' f2 g2 (g1 x)) a1) =
pusha1 a1
      apply (Pushout_rec_beta_pglue (f := f1) (g := pushl' f2 g2 o g1)).
    Defined.

    Definition pushout_assoc_right_rec_beta_pgluerr a2
      : ap pushout_assoc_right_rec (pgluerr a2) = pusha2 a2.
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
pushrl:= pushl' f1 (pushl' f2 g2 o g1): B -> pushout_assoc_right
pushrm:= pushr' f1 (pushl' f2 g2 o g1) o pushl' f2 g2: C -> pushout_assoc_right
pushrr:= pushr' f1 (pushl' f2 g2 o g1) o pushr' f2 g2: D -> pushout_assoc_right
pgluerl:= fun a1 : A1 =>
pglue' f1 (pushl' f2 g2 o g1) a1: forall a1 : A1,
pushrl (f1 a1) = pushrm (g1 a1)
pgluerr:= fun a2 : A2 =>
ap (pushr' f1 (pushl' f2 g2 o g1))
  (pglue' f2 g2 a2): forall a2 : A2,
pushrm (f2 a2) = pushrr (g2 a2)
P: Type
pushb: B -> P
pushc: C -> P
pushd: D -> P
pusha1: forall a1 : A1, pushb (f1 a1) = pushc (g1 a1)
pusha2: forall a2 : A2, pushc (f2 a2) = pushd (g2 a2)
a2: A2
ap pushout_assoc_right_rec (pgluerr a2) = pusha2 a2
    Proof.
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
pushrl:= pushl' f1 (pushl' f2 g2 o g1): B -> pushout_assoc_right
pushrm:= pushr' f1 (pushl' f2 g2 o g1) o pushl' f2 g2: C -> pushout_assoc_right
pushrr:= pushr' f1 (pushl' f2 g2 o g1) o pushr' f2 g2: D -> pushout_assoc_right
pgluerl:= fun a1 : A1 =>
pglue' f1 (pushl' f2 g2 o g1) a1: forall a1 : A1,
pushrl (f1 a1) = pushrm (g1 a1)
pgluerr:= fun a2 : A2 =>
ap (pushr' f1 (pushl' f2 g2 o g1))
  (pglue' f2 g2 a2): forall a2 : A2,
pushrm (f2 a2) = pushrr (g2 a2)
P: Type
pushb: B -> P
pushc: C -> P
pushd: D -> P
pusha1: forall a1 : A1, pushb (f1 a1) = pushc (g1 a1)
pusha2: forall a2 : A2, pushc (f2 a2) = pushd (g2 a2)
a2: A2
ap pushout_assoc_right_rec (pgluerr a2) = pusha2 a2
      unfold pgluerr.
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
pushrl:= pushl' f1 (pushl' f2 g2 o g1): B -> pushout_assoc_right
pushrm:= pushr' f1 (pushl' f2 g2 o g1) o pushl' f2 g2: C -> pushout_assoc_right
pushrr:= pushr' f1 (pushl' f2 g2 o g1) o pushr' f2 g2: D -> pushout_assoc_right
pgluerl:= fun a1 : A1 =>
pglue' f1 (pushl' f2 g2 o g1) a1: forall a1 : A1,
pushrl (f1 a1) = pushrm (g1 a1)
pgluerr:= fun a2 : A2 =>
ap (pushr' f1 (pushl' f2 g2 o g1))
  (pglue' f2 g2 a2): forall a2 : A2,
pushrm (f2 a2) = pushrr (g2 a2)
P: Type
pushb: B -> P
pushc: C -> P
pushd: D -> P
pusha1: forall a1 : A1, pushb (f1 a1) = pushc (g1 a1)
pusha2: forall a2 : A2, pushc (f2 a2) = pushd (g2 a2)
a2: A2
ap pushout_assoc_right_rec
  (ap (pushr' f1 (fun x : A1 => pushl' f2 g2 (g1 x)))
     (pglue' f2 g2 a2)) = pusha2 a2
      rewrite <- (ap_compose (pushr' f1 (pushl' f2 g2 o g1))
                             pushout_assoc_right_rec).
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
pushrl:= pushl' f1 (pushl' f2 g2 o g1): B -> pushout_assoc_right
pushrm:= pushr' f1 (pushl' f2 g2 o g1) o pushl' f2 g2: C -> pushout_assoc_right
pushrr:= pushr' f1 (pushl' f2 g2 o g1) o pushr' f2 g2: D -> pushout_assoc_right
pgluerl:= fun a1 : A1 =>
pglue' f1 (pushl' f2 g2 o g1) a1: forall a1 : A1,
pushrl (f1 a1) = pushrm (g1 a1)
pgluerr:= fun a2 : A2 =>
ap (pushr' f1 (pushl' f2 g2 o g1))
  (pglue' f2 g2 a2): forall a2 : A2,
pushrm (f2 a2) = pushrr (g2 a2)
P: Type
pushb: B -> P
pushc: C -> P
pushd: D -> P
pusha1: forall a1 : A1, pushb (f1 a1) = pushc (g1 a1)
pusha2: forall a2 : A2, pushc (f2 a2) = pushd (g2 a2)
a2: A2
ap
  (fun x : Pushout f2 g2 =>
   pushout_assoc_right_rec
     (pushr' f1 (fun x0 : A1 => pushl' f2 g2 (g1 x0))
        x)) (pglue' f2 g2 a2) = pusha2 a2
      change (ap (Pushout_rec P pushc pushd pusha2) (pglue' f2 g2 a2) = pusha2 a2).
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
pushrl:= pushl' f1 (pushl' f2 g2 o g1): B -> pushout_assoc_right
pushrm:= pushr' f1 (pushl' f2 g2 o g1) o pushl' f2 g2: C -> pushout_assoc_right
pushrr:= pushr' f1 (pushl' f2 g2 o g1) o pushr' f2 g2: D -> pushout_assoc_right
pgluerl:= fun a1 : A1 =>
pglue' f1 (pushl' f2 g2 o g1) a1: forall a1 : A1,
pushrl (f1 a1) = pushrm (g1 a1)
pgluerr:= fun a2 : A2 =>
ap (pushr' f1 (pushl' f2 g2 o g1))
  (pglue' f2 g2 a2): forall a2 : A2,
pushrm (f2 a2) = pushrr (g2 a2)
P: Type
pushb: B -> P
pushc: C -> P
pushd: D -> P
pusha1: forall a1 : A1, pushb (f1 a1) = pushc (g1 a1)
pusha2: forall a2 : A2, pushc (f2 a2) = pushd (g2 a2)
a2: A2
ap (Pushout_rec P pushc pushd pusha2)
  (pglue' f2 g2 a2) = pusha2 a2
      apply Pushout_rec_beta_pglue.
    Defined.

  End Pushout_Assoc_Right_Rec.

  Definition equiv_pushout_assoc
    : Pushout (pushr' f1 g1 o f2) g2 <~> Pushout f1 (pushl' f2 g2 o g1).
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
pushrl:= pushl' f1 (pushl' f2 g2 o g1): B -> pushout_assoc_right
pushrm:= pushr' f1 (pushl' f2 g2 o g1) o pushl' f2 g2: C -> pushout_assoc_right
pushrr:= pushr' f1 (pushl' f2 g2 o g1) o pushr' f2 g2: D -> pushout_assoc_right
pgluerl:= fun a1 : A1 =>
pglue' f1 (pushl' f2 g2 o g1) a1: forall a1 : A1,
pushrl (f1 a1) = pushrm (g1 a1)
pgluerr:= fun a2 : A2 =>
ap (pushr' f1 (pushl' f2 g2 o g1))
  (pglue' f2 g2 a2): forall a2 : A2,
pushrm (f2 a2) = pushrr (g2 a2)
Pushout (pushr' f1 g1 o f2) g2 <~>
Pushout f1 (pushl' f2 g2 o g1)
  Proof.
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
pushrl:= pushl' f1 (pushl' f2 g2 o g1): B -> pushout_assoc_right
pushrm:= pushr' f1 (pushl' f2 g2 o g1) o pushl' f2 g2: C -> pushout_assoc_right
pushrr:= pushr' f1 (pushl' f2 g2 o g1) o pushr' f2 g2: D -> pushout_assoc_right
pgluerl:= fun a1 : A1 =>
pglue' f1 (pushl' f2 g2 o g1) a1: forall a1 : A1,
pushrl (f1 a1) = pushrm (g1 a1)
pgluerr:= fun a2 : A2 =>
ap (pushr' f1 (pushl' f2 g2 o g1))
  (pglue' f2 g2 a2): forall a2 : A2,
pushrm (f2 a2) = pushrr (g2 a2)
Pushout (pushr' f1 g1 o f2) g2 <~>
Pushout f1 (pushl' f2 g2 o g1)
    srefine (equiv_adjointify _ _ _ _).
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
pushrl:= pushl' f1 (pushl' f2 g2 o g1): B -> pushout_assoc_right
pushrm:= pushr' f1 (pushl' f2 g2 o g1) o pushl' f2 g2: C -> pushout_assoc_right
pushrr:= pushr' f1 (pushl' f2 g2 o g1) o pushr' f2 g2: D -> pushout_assoc_right
pgluerl:= fun a1 : A1 =>
pglue' f1 (pushl' f2 g2 o g1) a1: forall a1 : A1,
pushrl (f1 a1) = pushrm (g1 a1)
pgluerr:= fun a2 : A2 =>
ap (pushr' f1 (pushl' f2 g2 o g1))
  (pglue' f2 g2 a2): forall a2 : A2,
pushrm (f2 a2) = pushrr (g2 a2)
Pushout (pushr' f1 g1 o f2) g2 ->
Pushout f1 (pushl' f2 g2 o g1)
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
pushrl:= pushl' f1 (pushl' f2 g2 o g1): B -> pushout_assoc_right
pushrm:= pushr' f1 (pushl' f2 g2 o g1) o pushl' f2 g2: C -> pushout_assoc_right
pushrr:= pushr' f1 (pushl' f2 g2 o g1) o pushr' f2 g2: D -> pushout_assoc_right
pgluerl:= fun a1 : A1 =>
pglue' f1 (pushl' f2 g2 o g1) a1: forall a1 : A1,
pushrl (f1 a1) = pushrm (g1 a1)
pgluerr:= fun a2 : A2 =>
ap (pushr' f1 (pushl' f2 g2 o g1))
  (pglue' f2 g2 a2): forall a2 : A2,
pushrm (f2 a2) = pushrr (g2 a2)
Pushout f1 (pushl' f2 g2 o g1) ->
Pushout (pushr' f1 g1 o f2) g2
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
pushrl:= pushl' f1 (pushl' f2 g2 o g1): B -> pushout_assoc_right
pushrm:= pushr' f1 (pushl' f2 g2 o g1) o pushl' f2 g2: C -> pushout_assoc_right
pushrr:= pushr' f1 (pushl' f2 g2 o g1) o pushr' f2 g2: D -> pushout_assoc_right
pgluerl:= fun a1 : A1 =>
pglue' f1 (pushl' f2 g2 o g1) a1: forall a1 : A1,
pushrl (f1 a1) = pushrm (g1 a1)
pgluerr:= fun a2 : A2 =>
ap (pushr' f1 (pushl' f2 g2 o g1))
  (pglue' f2 g2 a2): forall a2 : A2,
pushrm (f2 a2) = pushrr (g2 a2)
?f o ?g == idmap
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
pushrl:= pushl' f1 (pushl' f2 g2 o g1): B -> pushout_assoc_right
pushrm:= pushr' f1 (pushl' f2 g2 o g1) o pushl' f2 g2: C -> pushout_assoc_right
pushrr:= pushr' f1 (pushl' f2 g2 o g1) o pushr' f2 g2: D -> pushout_assoc_right
pgluerl:= fun a1 : A1 =>
pglue' f1 (pushl' f2 g2 o g1) a1: forall a1 : A1,
pushrl (f1 a1) = pushrm (g1 a1)
pgluerr:= fun a2 : A2 =>
ap (pushr' f1 (pushl' f2 g2 o g1))
  (pglue' f2 g2 a2): forall a2 : A2,
pushrm (f2 a2) = pushrr (g2 a2)
?g o ?f == idmap
    -
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
pushrl:= pushl' f1 (pushl' f2 g2 o g1): B -> pushout_assoc_right
pushrm:= pushr' f1 (pushl' f2 g2 o g1) o pushl' f2 g2: C -> pushout_assoc_right
pushrr:= pushr' f1 (pushl' f2 g2 o g1) o pushr' f2 g2: D -> pushout_assoc_right
pgluerl:= fun a1 : A1 =>
pglue' f1 (pushl' f2 g2 o g1) a1: forall a1 : A1,
pushrl (f1 a1) = pushrm (g1 a1)
pgluerr:= fun a2 : A2 =>
ap (pushr' f1 (pushl' f2 g2 o g1))
  (pglue' f2 g2 a2): forall a2 : A2,
pushrm (f2 a2) = pushrr (g2 a2)
Pushout (pushr' f1 g1 o f2) g2 ->
Pushout f1 (pushl' f2 g2 o g1) exact (pushout_assoc_left_rec _ pushrl pushrm pushrr pgluerl pgluerr).
    -
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
pushrl:= pushl' f1 (pushl' f2 g2 o g1): B -> pushout_assoc_right
pushrm:= pushr' f1 (pushl' f2 g2 o g1) o pushl' f2 g2: C -> pushout_assoc_right
pushrr:= pushr' f1 (pushl' f2 g2 o g1) o pushr' f2 g2: D -> pushout_assoc_right
pgluerl:= fun a1 : A1 =>
pglue' f1 (pushl' f2 g2 o g1) a1: forall a1 : A1,
pushrl (f1 a1) = pushrm (g1 a1)
pgluerr:= fun a2 : A2 =>
ap (pushr' f1 (pushl' f2 g2 o g1))
  (pglue' f2 g2 a2): forall a2 : A2,
pushrm (f2 a2) = pushrr (g2 a2)
Pushout f1 (pushl' f2 g2 o g1) ->
Pushout (pushr' f1 g1 o f2) g2 exact (pushout_assoc_right_rec _ pushll pushlm pushlr pgluell pgluelr).
    -
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
pushrl:= pushl' f1 (pushl' f2 g2 o g1): B -> pushout_assoc_right
pushrm:= pushr' f1 (pushl' f2 g2 o g1) o pushl' f2 g2: C -> pushout_assoc_right
pushrr:= pushr' f1 (pushl' f2 g2 o g1) o pushr' f2 g2: D -> pushout_assoc_right
pgluerl:= fun a1 : A1 =>
pglue' f1 (pushl' f2 g2 o g1) a1: forall a1 : A1,
pushrl (f1 a1) = pushrm (g1 a1)
pgluerr:= fun a2 : A2 =>
ap (pushr' f1 (pushl' f2 g2 o g1))
  (pglue' f2 g2 a2): forall a2 : A2,
pushrm (f2 a2) = pushrr (g2 a2)
pushout_assoc_left_rec pushout_assoc_right pushrl
  pushrm pushrr pgluerl pgluerr
o pushout_assoc_right_rec pushout_assoc_left pushll
    pushlm pushlr pgluell pgluelr == idmap abstract (
      srefine (pushout_assoc_right_ind
                 _ (fun _ => 1) (fun _ => 1) (fun _ => 1) _ _);
        intros; simpl; rewrite transport_paths_FlFr, ap_compose;
      [ rewrite pushout_assoc_right_rec_beta_pgluerl,
        pushout_assoc_left_rec_beta_pgluell
      | rewrite pushout_assoc_right_rec_beta_pgluerr,
        pushout_assoc_left_rec_beta_pgluelr ];
      rewrite concat_p1, ap_idmap; apply concat_Vp ).
    -
A1, A2, B, C, D: Type
f1: A1 -> B
g1: A1 -> C
f2: A2 -> C
g2: A2 -> D
pushll:= pushl' (pushr' f1 g1 o f2) g2 o pushl' f1 g1: B -> pushout_assoc_left
pushlm:= pushl' (pushr' f1 g1 o f2) g2 o pushr' f1 g1: C -> pushout_assoc_left
pushlr:= pushr' (pushr' f1 g1 o f2) g2: D -> pushout_assoc_left
pgluell:= fun a1 : A1 =>
ap (pushl' (pushr' f1 g1 o f2) g2)
  (pglue' f1 g1 a1): forall a1 : A1,
pushll (f1 a1) = pushlm (g1 a1)
pgluelr:= fun a2 : A2 =>
pglue' (pushr' f1 g1 o f2) g2 a2: forall a2 : A2,
pushlm (f2 a2) = pushlr (g2 a2)
pushrl:= pushl' f1 (pushl' f2 g2 o g1): B -> pushout_assoc_right
pushrm:= pushr' f1 (pushl' f2 g2 o g1) o pushl' f2 g2: C -> pushout_assoc_right
pushrr:= pushr' f1 (pushl' f2 g2 o g1) o pushr' f2 g2: D -> pushout_assoc_right
pgluerl:= fun a1 : A1 =>
pglue' f1 (pushl' f2 g2 o g1) a1: forall a1 : A1,
pushrl (f1 a1) = pushrm (g1 a1)
pgluerr:= fun a2 : A2 =>
ap (pushr' f1 (pushl' f2 g2 o g1))
  (pglue' f2 g2 a2): forall a2 : A2,
pushrm (f2 a2) = pushrr (g2 a2)
pushout_assoc_right_rec pushout_assoc_left pushll
  pushlm pushlr pgluell pgluelr
o pushout_assoc_left_rec pushout_assoc_right pushrl
    pushrm pushrr pgluerl pgluerr == idmap abstract (
      srefine (pushout_assoc_left_ind
                 _ (fun _ => 1) (fun _ => 1) (fun _ => 1) _ _);
        intros; simpl; rewrite transport_paths_FlFr, ap_compose;
      [ rewrite pushout_assoc_left_rec_beta_pgluell,
        pushout_assoc_right_rec_beta_pgluerl
      | rewrite pushout_assoc_left_rec_beta_pgluelr,
        pushout_assoc_right_rec_beta_pgluerr ];
      rewrite concat_p1, ap_idmap; apply concat_Vp ).
  Defined.

End PushoutAssoc.

(** ** Pushouts of equvialences are equivalences *)

Global Instance isequiv_pushout_isequiv {A B C} (f : A -> B) (g : A -> C)
       `{IsEquiv _ _ f} : IsEquiv (pushr' f g).
A, B, C: Type
f: A -> B
g: A -> C
H: IsEquiv f
IsEquiv (pushr' f g)
Proof.
A, B, C: Type
f: A -> B
g: A -> C
H: IsEquiv f
IsEquiv (pushr' f g)
  srefine (isequiv_adjointify _ _ _ _).
A, B, C: Type
f: A -> B
g: A -> C
H: IsEquiv f
Pushout f g -> C
A, B, C: Type
f: A -> B
g: A -> C
H: IsEquiv f
pushr' f g o ?g == idmap
A, B, C: Type
f: A -> B
g: A -> C
H: IsEquiv f
?g o pushr' f g == idmap
  -
A, B, C: Type
f: A -> B
g: A -> C
H: IsEquiv f
Pushout f g -> C srefine (Pushout_rec C (g o f^-1) idmap _).
A, B, C: Type
f: A -> B
g: A -> C
H: IsEquiv f
forall a : A, (g o f^-1) (f a) = idmap (g a)
    intros a; cbn; apply ap, eissect.
  -
A, B, C: Type
f: A -> B
g: A -> C
H: IsEquiv f
pushr' f g
o Pushout_rec C (g o f^-1) idmap
    (fun a : A =>
     ap g (eissect f a)
     :
     (g o f^-1) (f a) = idmap (g a)) == idmap srefine (Pushout_ind _ _ _ _); cbn.
A, B, C: Type
f: A -> B
g: A -> C
H: IsEquiv f
forall b : B,
pushr' f g
  (Pushout_rec C (fun x : B => g (f^-1 x)) idmap
     (fun a : A => ap g (eissect f a)) (pushl b)) =
pushl b
A, B, C: Type
f: A -> B
g: A -> C
H: IsEquiv f
forall c : C,
pushr' f g
  (Pushout_rec C (fun x : B => g (f^-1 x)) idmap
     (fun a : A => ap g (eissect f a)) (pushr c)) =
pushr c
A, B, C: Type
f: A -> B
g: A -> C
H: IsEquiv f
forall a : A,
transport
  (fun w : Pushout f g =>
   pushr' f g
     (Pushout_rec C (fun x : B => g (f^-1 x)) idmap
        (fun a0 : A => ap g (eissect f a0)) w) = w)
  (pglue a) (?Goal (f a)) = ?Goal0 (g a)
    +
A, B, C: Type
f: A -> B
g: A -> C
H: IsEquiv f
forall b : B,
pushr' f g
  (Pushout_rec C (fun x : B => g (f^-1 x)) idmap
     (fun a : A => ap g (eissect f a)) (pushl b)) =
pushl b intros b; change (pushr' f g (g (f^-1 b)) = pushl b).
A, B, C: Type
f: A -> B
g: A -> C
H: IsEquiv f
b: B
pushr' f g (g (f^-1 b)) = pushl b
      transitivity (pushl' f g (f (f^-1 b))).
A, B, C: Type
f: A -> B
g: A -> C
H: IsEquiv f
b: B
pushr' f g (g (f^-1 b)) = pushl' f g (f (f^-1 b))
A, B, C: Type
f: A -> B
g: A -> C
H: IsEquiv f
b: B
pushl' f g (f (f^-1 b)) = pushl b
      *
A, B, C: Type
f: A -> B
g: A -> C
H: IsEquiv f
b: B
pushr' f g (g (f^-1 b)) = pushl' f g (f (f^-1 b)) symmetry; apply pglue.
      *
A, B, C: Type
f: A -> B
g: A -> C
H: IsEquiv f
b: B
pushl' f g (f (f^-1 b)) = pushl b apply ap, eisretr.
    +
A, B, C: Type
f: A -> B
g: A -> C
H: IsEquiv f
forall c : C,
pushr' f g
  (Pushout_rec C (fun x : B => g (f^-1 x)) idmap
     (fun a : A => ap g (eissect f a)) (pushr c)) =
pushr c intros c; reflexivity.
    +
A, B, C: Type
f: A -> B
g: A -> C
H: IsEquiv f
forall a : A,
transport
  (fun w : Pushout f g =>
   pushr' f g
     (Pushout_rec C (fun x : B => g (f^-1 x)) idmap
        (fun a0 : A => ap g (eissect f a0)) w) = w)
  (pglue a)
  ((fun b : B =>
    (pglue (f^-1 b))^ @ ap pushl (eisretr f b)) (f a)) =
(fun c : C => 1) (g a) intros a.
A, B, C: Type
f: A -> B
g: A -> C
H: IsEquiv f
a: A
transport
  (fun w : Pushout f g =>
   pushr' f g
     (Pushout_rec C (fun x : B => g (f^-1 x)) idmap
        (fun a : A => ap g (eissect f a)) w) = w)
  (pglue a)
  ((fun b : B =>
    (pglue (f^-1 b))^ @ ap pushl (eisretr f b)) (f a)) =
(fun c : C => 1) (g a)
      abstract (
      rewrite transport_paths_FlFr, ap_compose, !concat_pp_p;
      apply moveR_Vp; apply moveR_Vp;
      rewrite Pushout_rec_beta_pglue, eisadj, ap_idmap, concat_p1;
      rewrite <- ap_compose, <- (ap_compose g (pushr' f g));
      exact (concat_Ap (pglue' f g) (eissect f a)) ).
  -
A, B, C: Type
f: A -> B
g: A -> C
H: IsEquiv f
Pushout_rec C (g o f^-1) idmap
  (fun a : A =>
   ap g (eissect f a) : (g o f^-1) (f a) = idmap (g a))
o pushr' f g == idmap intros c; reflexivity.
Defined.

Global Instance isequiv_pushout_isequiv' {A B C} (f : A -> B) (g : A -> C)
       `{IsEquiv _ _ g} : IsEquiv (pushl' f g).
A, B, C: Type
f: A -> B
g: A -> C
H: IsEquiv g
IsEquiv (pushl' f g)
Proof.
A, B, C: Type
f: A -> B
g: A -> C
H: IsEquiv g
IsEquiv (pushl' f g)
  srefine (isequiv_adjointify _ _ _ _).
A, B, C: Type
f: A -> B
g: A -> C
H: IsEquiv g
Pushout f g -> B
A, B, C: Type
f: A -> B
g: A -> C
H: IsEquiv g
pushl' f g o ?g == idmap
A, B, C: Type
f: A -> B
g: A -> C
H: IsEquiv g
?g o pushl' f g == idmap
  -
A, B, C: Type
f: A -> B
g: A -> C
H: IsEquiv g
Pushout f g -> B srefine (Pushout_rec B idmap (f o g^-1) _).
A, B, C: Type
f: A -> B
g: A -> C
H: IsEquiv g
forall a : A, idmap (f a) = (f o g^-1) (g a)
    intros a; cbn.
A, B, C: Type
f: A -> B
g: A -> C
H: IsEquiv g
a: A
f a = f (g^-1 (g a)) symmetry; apply ap, eissect.
  -
A, B, C: Type
f: A -> B
g: A -> C
H: IsEquiv g
pushl' f g
o Pushout_rec B idmap (f o g^-1)
    (fun a : A =>
     (ap f (eissect g a))^
     :
     idmap (f a) = (f o g^-1) (g a)) == idmap srefine (Pushout_ind _ _ _ _); cbn.
A, B, C: Type
f: A -> B
g: A -> C
H: IsEquiv g
forall b : B,
pushl' f g
  (Pushout_rec B idmap (fun x : C => f (g^-1 x))
     (fun a : A => (ap f (eissect g a))^) (pushl b)) =
pushl b
A, B, C: Type
f: A -> B
g: A -> C
H: IsEquiv g
forall c : C,
pushl' f g
  (Pushout_rec B idmap (fun x : C => f (g^-1 x))
     (fun a : A => (ap f (eissect g a))^) (pushr c)) =
pushr c
A, B, C: Type
f: A -> B
g: A -> C
H: IsEquiv g
forall a : A,
transport
  (fun w : Pushout f g =>
   pushl' f g
     (Pushout_rec B idmap (fun x : C => f (g^-1 x))
        (fun a0 : A => (ap f (eissect g a0))^) w) = w)
  (pglue a) (?Goal (f a)) = ?Goal0 (g a)
    +
A, B, C: Type
f: A -> B
g: A -> C
H: IsEquiv g
forall b : B,
pushl' f g
  (Pushout_rec B idmap (fun x : C => f (g^-1 x))
     (fun a : A => (ap f (eissect g a))^) (pushl b)) =
pushl b intros b; reflexivity.
    +
A, B, C: Type
f: A -> B
g: A -> C
H: IsEquiv g
forall c : C,
pushl' f g
  (Pushout_rec B idmap (fun x : C => f (g^-1 x))
     (fun a : A => (ap f (eissect g a))^) (pushr c)) =
pushr c intros c; change (pushl' f g (f (g^-1 c)) = pushr c).
A, B, C: Type
f: A -> B
g: A -> C
H: IsEquiv g
c: C
pushl' f g (f (g^-1 c)) = pushr c
      transitivity (pushr' f g (g (g^-1 c))).
A, B, C: Type
f: A -> B
g: A -> C
H: IsEquiv g
c: C
pushl' f g (f (g^-1 c)) = pushr' f g (g (g^-1 c))
A, B, C: Type
f: A -> B
g: A -> C
H: IsEquiv g
c: C
pushr' f g (g (g^-1 c)) = pushr c
      *
A, B, C: Type
f: A -> B
g: A -> C
H: IsEquiv g
c: C
pushl' f g (f (g^-1 c)) = pushr' f g (g (g^-1 c)) apply pglue.
      *
A, B, C: Type
f: A -> B
g: A -> C
H: IsEquiv g
c: C
pushr' f g (g (g^-1 c)) = pushr c apply ap, eisretr.
    +
A, B, C: Type
f: A -> B
g: A -> C
H: IsEquiv g
forall a : A,
transport
  (fun w : Pushout f g =>
   pushl' f g
     (Pushout_rec B idmap (fun x : C => f (g^-1 x))
        (fun a0 : A => (ap f (eissect g a0))^) w) = w)
  (pglue a) ((fun b : B => 1) (f a)) =
(fun c : C => pglue (g^-1 c) @ ap pushr (eisretr g c))
  (g a) intros a.
A, B, C: Type
f: A -> B
g: A -> C
H: IsEquiv g
a: A
transport
  (fun w : Pushout f g =>
   pushl' f g
     (Pushout_rec B idmap (fun x : C => f (g^-1 x))
        (fun a : A => (ap f (eissect g a))^) w) = w)
  (pglue a) ((fun b : B => 1) (f a)) =
(fun c : C => pglue (g^-1 c) @ ap pushr (eisretr g c))
  (g a)
      abstract (
      rewrite transport_paths_FlFr, ap_compose, !concat_pp_p;
      apply moveR_Vp;
      rewrite Pushout_rec_beta_pglue, eisadj, ap_idmap, concat_1p, ap_V;
      apply moveL_Vp;
      rewrite <- !ap_compose;
      exact (concat_Ap (pglue' f g) (eissect g a)) ).
  -
A, B, C: Type
f: A -> B
g: A -> C
H: IsEquiv g
Pushout_rec B idmap (f o g^-1)
  (fun a : A =>
   (ap f (eissect g a))^
   :
   idmap (f a) = (f o g^-1) (g a)) o pushl' f g ==
idmap intros c; reflexivity.
Defined.

(** ** Flattening lemma for pushouts *)

(** The flattening lemma for pushouts follows from the flattening lemma for coequalizers. *)

Section Flattening.

  Context `{Univalence} {A B C} {f : A -> B} {g : A -> C}
    (F : B -> Type) (G : C -> Type) (e : forall a, F (f a) <~> G (g a)).

  Definition pushout_flatten_fam : Pushout f g -> Type
    := Pushout_rec Type F G (fun a => path_universe (e a)).

  (** In this result, the vertex of the pushout is taken to be [{ a : A & F(f(a))}], the pullback of [F] along [f]. *)
  Definition equiv_pushout_flatten
    : sig pushout_flatten_fam
    <~> Pushout (functor_sigma f (fun _ => idmap)) (functor_sigma g e).
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
F: B -> Type
G: C -> Type
e: forall a : A, F (f a) <~> G (g a)
{x : _ & pushout_flatten_fam x} <~>
Pushout (functor_sigma f (fun a : A => idmap))
  (functor_sigma g (fun a : A => e a))
  Proof.
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
F: B -> Type
G: C -> Type
e: forall a : A, F (f a) <~> G (g a)
{x : _ & pushout_flatten_fam x} <~>
Pushout (functor_sigma f (fun a : A => idmap))
  (functor_sigma g (fun a : A => e a))
    unfold pushout_flatten_fam.
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
F: B -> Type
G: C -> Type
e: forall a : A, F (f a) <~> G (g a)
{x : _ &
Pushout_rec Type F G
  (fun a : A => path_universe (e a)) x} <~>
Pushout (functor_sigma f (fun a : A => idmap))
  (functor_sigma g (fun a : A => e a))
    refine (_ oE equiv_coeq_flatten _ _).
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
F: B -> Type
G: C -> Type
e: forall a : A, F (f a) <~> G (g a)
Coeq
  (functor_sigma (fun x : A => inl (f x))
     (fun a : A => idmap))
  (functor_sigma (fun x : A => inr (g x))
     (fun b : A => e b)) <~>
Pushout (functor_sigma f (fun a : A => idmap))
  (functor_sigma g (fun a : A => e a))
    unfold Pushout.
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
F: B -> Type
G: C -> Type
e: forall a : A, F (f a) <~> G (g a)
Coeq
  (functor_sigma (fun x : A => inl (f x))
     (fun a : A => idmap))
  (functor_sigma (fun x : A => inr (g x))
     (fun b : A => e b)) <~>
Coeq
  (fun x : {H : A & F (f H)} =>
   inl (functor_sigma f (fun a : A => idmap) x))
  (fun x : {H : A & F (f H)} =>
   inr (functor_sigma g (fun a : A => e a) x))
    snrapply equiv_functor_coeq'.
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
F: B -> Type
G: C -> Type
e: forall a : A, F (f a) <~> G (g a)
{H : A & sum_rec Type F G (inl (f H))} <~>
{H : A & F (f H)}
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
F: B -> Type
G: C -> Type
e: forall a : A, F (f a) <~> G (g a)
{x : _ & sum_rec Type F G x} <~>
{x : _ & F x} + {x : _ & G x}
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
F: B -> Type
G: C -> Type
e: forall a : A, F (f a) <~> G (g a)
?k
o functor_sigma (fun x : A => inl (f x))
    (fun a : A => idmap) ==
(fun x : {H : A & F (f H)} =>
 inl (functor_sigma f (fun a : A => idmap) x)) o ?h
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
F: B -> Type
G: C -> Type
e: forall a : A, F (f a) <~> G (g a)
?k
o functor_sigma (fun x : A => inr (g x))
    (fun b : A => e b) ==
(fun x : {H : A & F (f H)} =>
 inr (functor_sigma g (fun a : A => e a) x)) o ?h
    -
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
F: B -> Type
G: C -> Type
e: forall a : A, F (f a) <~> G (g a)
{H : A & sum_rec Type F G (inl (f H))} <~>
{H : A & F (f H)} reflexivity.
    -
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
F: B -> Type
G: C -> Type
e: forall a : A, F (f a) <~> G (g a)
{x : _ & sum_rec Type F G x} <~>
{x : _ & F x} + {x : _ & G x} apply equiv_sigma_sum.
    -
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
F: B -> Type
G: C -> Type
e: forall a : A, F (f a) <~> G (g a)
equiv_sigma_sum B C (sum_rec Type F G)
o functor_sigma (fun x : A => inl (f x))
    (fun a : A => idmap) ==
(fun x : {H : A & F (f H)} =>
 inl (functor_sigma f (fun a : A => idmap) x))
o 1%equiv reflexivity.
    -
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
F: B -> Type
G: C -> Type
e: forall a : A, F (f a) <~> G (g a)
equiv_sigma_sum B C (sum_rec Type F G)
o functor_sigma (fun x : A => inr (g x))
    (fun b : A => e b) ==
(fun x : {H : A & F (f H)} =>
 inr (functor_sigma g (fun a : A => e a) x)) o 1%equiv reflexivity.
  Defined.

End Flattening.