From HoTT Require Import Basics.From HoTT Require Import Basics.
Require Import Types.
Require Import Diagrams.Graph.
Require Import Diagrams.Diagram.
Require Import Diagrams.Span.
Require Import Diagrams.Cocone.
Require Import Colimits.Colimit.

(* We require this now, but will import later. *)
Require Colimits.Pushout.

Local Open Scope path_scope.

(** * Pushout as a colimit *)

(** In this file, we define [PO] the pushout of two maps as the colimit of a particular diagram, and then show that it is equivalent to [pushout] the primitive pushout defined as an HIT. *)


(** ** [PO] *)
Section PO.

  Context {A B C : Type}.

  Definition Build_span_cocone {f : A -> B} {g : A -> C} {Z : Type}
             (inl' : B -> Z) (inr' : C -> Z)
             (pp' : inl' o f == inr' o g)
    : Cocone (span f g) Z.
A, B, C: Type
f: A -> B
g: A -> C
Z: Type
inl': B -> Z
inr': C -> Z
pp': inl' o f == inr' o g
Cocone (span f g) Z
  Proof.
A, B, C: Type
f: A -> B
g: A -> C
Z: Type
inl': B -> Z
inr': C -> Z
pp': inl' o f == inr' o g
Cocone (span f g) Z
    srapply Build_Cocone.
A, B, C: Type
f: A -> B
g: A -> C
Z: Type
inl': B -> Z
inr': C -> Z
pp': inl' o f == inr' o g
forall i : span_graph, span f g i -> Z
A, B, C: Type
f: A -> B
g: A -> C
Z: Type
inl': B -> Z
inr': C -> Z
pp': inl' o f == inr' o g
forall (i j : span_graph) (g0 : span_graph i j),
?legs j o (span f g) _f g0 == ?legs i
    -
A, B, C: Type
f: A -> B
g: A -> C
Z: Type
inl': B -> Z
inr': C -> Z
pp': inl' o f == inr' o g
forall i : span_graph, span f g i -> Z intros [|[]]; [ exact (inr' o g) | exact inl' | exact inr' ].
    -
A, B, C: Type
f: A -> B
g: A -> C
Z: Type
inl': B -> Z
inr': C -> Z
pp': inl' o f == inr' o g
forall (i j : span_graph) (g0 : span_graph i j),
(fun i0 : span_graph =>
 match i0 as s return (span f g s -> Z) with
 | inl u => unit_name (inr' o g) u
 | inr b =>
     (fun b0 : Bool =>
      if b0 as b1 return (span f g (inr b1) -> Z) then inl' else inr') b
 end) j
o (span f g) _f g0 ==
(fun i0 : span_graph =>
 match i0 as s return (span f g s -> Z) with
 | inl u => unit_name (inr' o g) u
 | inr b =>
     (fun b0 : Bool =>
      if b0 as b1 return (span f g (inr b1) -> Z) then inl' else inr') b
 end) i intros [u|b] [u'|b'] []; cbn.
A, B, C: Type
f: A -> B
g: A -> C
Z: Type
inl': B -> Z
inr': C -> Z
pp': inl' o f == inr' o g
u: Unit
b': Bool
(fun x : A =>
 (if b' as b return ((if b then B else C) -> Z) then inl' else inr')
   ((if b' as b return (Unit -> A -> if b then B else C)
     then unit_name f
     else unit_name g) tt x)) ==
(fun x : A => inr' (g x)) destruct b'.
A, B, C: Type
f: A -> B
g: A -> C
Z: Type
inl': B -> Z
inr': C -> Z
pp': inl' o f == inr' o g
u: Unit
(fun x : A => inl' (f x)) == (fun x : A => inr' (g x))
A, B, C: Type
f: A -> B
g: A -> C
Z: Type
inl': B -> Z
inr': C -> Z
pp': inl' o f == inr' o g
u: Unit
(fun x : A => inr' (g x)) == (fun x : A => inr' (g x))
      +
A, B, C: Type
f: A -> B
g: A -> C
Z: Type
inl': B -> Z
inr': C -> Z
pp': inl' o f == inr' o g
u: Unit
(fun x : A => inl' (f x)) == (fun x : A => inr' (g x)) exact pp'.
      +
A, B, C: Type
f: A -> B
g: A -> C
Z: Type
inl': B -> Z
inr': C -> Z
pp': inl' o f == inr' o g
u: Unit
(fun x : A => inr' (g x)) == (fun x : A => inr' (g x)) reflexivity.
  Defined.

  Definition pol' {f : A -> B} {g : A -> C} {Z} (Co : Cocone (span f g) Z)
    : B -> Z
    := legs Co (inr true).
  Definition por' {f : A -> B} {g : A -> C} {Z} (Co : Cocone (span f g) Z)
    : C -> Z
    := legs Co (inr false).
  Definition popp' {f : A -> B} {g : A -> C} {Z} (Co : Cocone (span f g) Z)
    : pol' Co o f == por' Co o g
    := fun x => legs_comm Co (inl tt) (inr true) tt x
                @ (legs_comm Co (inl tt) (inr false) tt x)^.

  Definition is_PO (f : A -> B) (g : A -> C) := IsColimit (span f g).
  Definition PO (f : A -> B) (g : A -> C) := Colimit (span f g).

  Context {f : A -> B} {g : A -> C}.

  Definition pol : B -> PO f g := colim (D:=span f g) (inr true).
  Definition por : C -> PO f g := colim (D:=span f g) (inr false).

  Definition popp (a : A) : pol (f a) = por (g a)
    := colimp (D:=span f g) (inl tt) (inr true) tt a
          @ (colimp (D:=span f g) (inl tt) (inr false) tt a)^.

  (** We next define the eliminators [PO_ind] and [PO_rec]. To make later proof terms smaller, we define two things we'll need. *)
  Definition PO_ind_obj (P : PO f g -> Type) (l' : forall b, P (pol b))
    (r' : forall c, P (por c))
    : forall (i : span_graph) (x : obj (span f g) i), P (colim i x).
A, B, C: Type
f: A -> B
g: A -> C
P: PO f g -> Type
l': forall b : B, P (pol b)
r': forall c : C, P (por c)
forall (i : span_graph) (x : span f g i), P (colim i x)
  Proof.
A, B, C: Type
f: A -> B
g: A -> C
P: PO f g -> Type
l': forall b : B, P (pol b)
r': forall c : C, P (por c)
forall (i : span_graph) (x : span f g i), P (colim i x)
    intros [u|[]] x; cbn.
A, B, C: Type
f: A -> B
g: A -> C
P: PO f g -> Type
l': forall b : B, P (pol b)
r': forall c : C, P (por c)
u: Unit
x: span f g (inl u)
P (colim (inl u) x)
A, B, C: Type
f: A -> B
g: A -> C
P: PO f g -> Type
l': forall b : B, P (pol b)
r': forall c : C, P (por c)
x: span f g (inr true)
P (colim (inr true) x)
A, B, C: Type
f: A -> B
g: A -> C
P: PO f g -> Type
l': forall b : B, P (pol b)
r': forall c : C, P (por c)
x: span f g (inr false)
P (colim (inr false) x)
    -
A, B, C: Type
f: A -> B
g: A -> C
P: PO f g -> Type
l': forall b : B, P (pol b)
r': forall c : C, P (por c)
u: Unit
x: span f g (inl u)
P (colim (inl u) x) exact (@colimp _ (span f g) (inl u) (inr true) tt x # l' (f x)).
    -
A, B, C: Type
f: A -> B
g: A -> C
P: PO f g -> Type
l': forall b : B, P (pol b)
r': forall c : C, P (por c)
x: span f g (inr true)
P (colim (inr true) x) exact (l' x).
    -
A, B, C: Type
f: A -> B
g: A -> C
P: PO f g -> Type
l': forall b : B, P (pol b)
r': forall c : C, P (por c)
x: span f g (inr false)
P (colim (inr false) x) exact (r' x).
  Defined.

  Definition PO_ind_arr (P : PO f g -> Type) (l' : forall b, P (pol b))
    (r' : forall c, P (por c)) (pp' : forall a, popp a # l' (f a) = r' (g a))
    : forall (i j : span_graph) (e : span_graph i j) (ar : span f g i),
      transport P (colimp i j e ar) (PO_ind_obj P l' r' j (((span f g) _f e) ar)) =
        PO_ind_obj P l' r' i ar.
A, B, C: Type
f: A -> B
g: A -> C
P: PO f g -> Type
l': forall b : B, P (pol b)
r': forall c : C, P (por c)
pp': forall a : A, transport P (popp a) (l' (f a)) = r' (g a)
forall (i j : span_graph) (e : span_graph i j) (ar : span f g i),
transport P (colimp i j e ar) (PO_ind_obj P l' r' j (((span f g) _f e) ar)) =
PO_ind_obj P l' r' i ar
  Proof.
A, B, C: Type
f: A -> B
g: A -> C
P: PO f g -> Type
l': forall b : B, P (pol b)
r': forall c : C, P (por c)
pp': forall a : A, transport P (popp a) (l' (f a)) = r' (g a)
forall (i j : span_graph) (e : span_graph i j) (ar : span f g i),
transport P (colimp i j e ar) (PO_ind_obj P l' r' j (((span f g) _f e) ar)) =
PO_ind_obj P l' r' i ar
    intros [u|b] [u'|b'] []; cbn.
A, B, C: Type
f: A -> B
g: A -> C
P: PO f g -> Type
l': forall b : B, P (pol b)
r': forall c : C, P (por c)
pp': forall a : A, transport P (popp a) (l' (f a)) = r' (g a)
u: Unit
b': Bool
forall ar : A,
transport P (colimp (inl u) (inr b') tt ar)
  ((if b' as b return (forall x : if b then B else C, P (colim (inr b) x))
    then fun x : B => l' x
    else fun x : C => r' x)
     ((if b' as b return (Unit -> A -> if b then B else C)
       then unit_name f
       else unit_name g) tt ar)) =
transport P (colimp (inl u) (inr true) tt ar) (l' (f ar))
    destruct b'; cbn.
A, B, C: Type
f: A -> B
g: A -> C
P: PO f g -> Type
l': forall b : B, P (pol b)
r': forall c : C, P (por c)
pp': forall a : A, transport P (popp a) (l' (f a)) = r' (g a)
u: Unit
forall ar : A,
transport P (colimp (inl u) (inr true) tt ar) (l' (f ar)) =
transport P (colimp (inl u) (inr true) tt ar) (l' (f ar))
A, B, C: Type
f: A -> B
g: A -> C
P: PO f g -> Type
l': forall b : B, P (pol b)
r': forall c : C, P (por c)
pp': forall a : A, transport P (popp a) (l' (f a)) = r' (g a)
u: Unit
forall ar : A,
transport P (colimp (inl u) (inr false) tt ar) (r' (g ar)) =
transport P (colimp (inl u) (inr true) tt ar) (l' (f ar))
    1: reflexivity.
A, B, C: Type
f: A -> B
g: A -> C
P: PO f g -> Type
l': forall b : B, P (pol b)
r': forall c : C, P (por c)
pp': forall a : A, transport P (popp a) (l' (f a)) = r' (g a)
u: Unit
forall ar : A,
transport P (colimp (inl u) (inr false) tt ar) (r' (g ar)) =
transport P (colimp (inl u) (inr true) tt ar) (l' (f ar))
    unfold popp in pp'.
A, B, C: Type
f: A -> B
g: A -> C
P: PO f g -> Type
l': forall b : B, P (pol b)
r': forall c : C, P (por c)
pp': forall a : A,
transport P
  (colimp (inl tt) (inr true) tt a @ (colimp (inl tt) (inr false) tt a)^)
  (l' (f a)) =
r' (g a)
u: Unit
forall ar : A,
transport P (colimp (inl u) (inr false) tt ar) (r' (g ar)) =
transport P (colimp (inl u) (inr true) tt ar) (l' (f ar))
    intro a.
A, B, C: Type
f: A -> B
g: A -> C
P: PO f g -> Type
l': forall b : B, P (pol b)
r': forall c : C, P (por c)
pp': forall a0 : A,
transport P
  (colimp (inl tt) (inr true) tt a0 @ (colimp (inl tt) (inr false) tt a0)^)
  (l' (f a0)) =
r' (g a0)
u: Unit
a: A
transport P (colimp (inl u) (inr false) tt a) (r' (g a)) =
transport P (colimp (inl u) (inr true) tt a) (l' (f a)) apply moveR_transport_p.
A, B, C: Type
f: A -> B
g: A -> C
P: PO f g -> Type
l': forall b : B, P (pol b)
r': forall c : C, P (por c)
pp': forall a0 : A,
transport P
  (colimp (inl tt) (inr true) tt a0 @ (colimp (inl tt) (inr false) tt a0)^)
  (l' (f a0)) =
r' (g a0)
u: Unit
a: A
r' (g a) =
transport P (colimp (inl u) (inr false) tt a)^
  (transport P (colimp (inl u) (inr true) tt a) (l' (f a)))
    rhs_V napply transport_pp.
A, B, C: Type
f: A -> B
g: A -> C
P: PO f g -> Type
l': forall b : B, P (pol b)
r': forall c : C, P (por c)
pp': forall a0 : A,
transport P
  (colimp (inl tt) (inr true) tt a0 @ (colimp (inl tt) (inr false) tt a0)^)
  (l' (f a0)) =
r' (g a0)
u: Unit
a: A
r' (g a) =
transport P
  (colimp (inl u) (inr true) tt a @ (colimp (inl u) (inr false) tt a)^)
  (l' (f a))
    destruct u.
A, B, C: Type
f: A -> B
g: A -> C
P: PO f g -> Type
l': forall b : B, P (pol b)
r': forall c : C, P (por c)
pp': forall a0 : A,
transport P
  (colimp (inl tt) (inr true) tt a0 @ (colimp (inl tt) (inr false) tt a0)^)
  (l' (f a0)) =
r' (g a0)
a: A
r' (g a) =
transport P
  (colimp (inl tt) (inr true) tt a @ (colimp (inl tt) (inr false) tt a)^)
  (l' (f a))
    symmetry; apply pp'.
  Defined.

  Definition PO_ind (P : PO f g -> Type) (l' : forall b, P (pol b))
    (r' : forall c, P (por c)) (pp' : forall a, popp a # l' (f a) = r' (g a))
    : forall w, P w
    := Colimit_ind P (PO_ind_obj P l' r') (PO_ind_arr P l' r' pp').

  Definition PO_ind_beta_pp (P : PO f g -> Type) (l' : forall b, P (pol b))
    (r' : forall c, P (por c)) (pp' : forall a, popp a # l' (f a) = r' (g a))
    : forall x, apD (PO_ind P l' r' pp') (popp x) = pp' x.
A, B, C: Type
f: A -> B
g: A -> C
P: PO f g -> Type
l': forall b : B, P (pol b)
r': forall c : C, P (por c)
pp': forall a : A, transport P (popp a) (l' (f a)) = r' (g a)
forall x : A, apD (PO_ind P l' r' pp') (popp x) = pp' x
  Proof.
A, B, C: Type
f: A -> B
g: A -> C
P: PO f g -> Type
l': forall b : B, P (pol b)
r': forall c : C, P (por c)
pp': forall a : A, transport P (popp a) (l' (f a)) = r' (g a)
forall x : A, apD (PO_ind P l' r' pp') (popp x) = pp' x
    intro x.
A, B, C: Type
f: A -> B
g: A -> C
P: PO f g -> Type
l': forall b : B, P (pol b)
r': forall c : C, P (por c)
pp': forall a : A, transport P (popp a) (l' (f a)) = r' (g a)
x: A
apD (PO_ind P l' r' pp') (popp x) = pp' x
    lhs napply apD_pp.
A, B, C: Type
f: A -> B
g: A -> C
P: PO f g -> Type
l': forall b : B, P (pol b)
r': forall c : C, P (por c)
pp': forall a : A, transport P (popp a) (l' (f a)) = r' (g a)
x: A
(transport_pp P (colimp (inl tt) (inr true) tt x)
   (colimp (inl tt) (inr false) tt x)^ (PO_ind P l' r' pp' (pol (f x))) @
 ap (transport P (colimp (inl tt) (inr false) tt x)^)
   (apD (PO_ind P l' r' pp') (colimp (inl tt) (inr true) tt x))) @
apD (PO_ind P l' r' pp') (colimp (inl tt) (inr false) tt x)^ = 
pp' x
    rewrite (Colimit_ind_beta_colimp P _ _ (inl tt) (inr true) tt x).
A, B, C: Type
f: A -> B
g: A -> C
P: PO f g -> Type
l': forall b : B, P (pol b)
r': forall c : C, P (por c)
pp': forall a : A, transport P (popp a) (l' (f a)) = r' (g a)
x: A
(transport_pp P (colimp (inl tt) (inr true) tt x)
   (colimp (inl tt) (inr false) tt x)^ (PO_ind P l' r' pp' (pol (f x))) @
 ap (transport P (colimp (inl tt) (inr false) tt x)^)
   (PO_ind_arr P l' r' pp' (inl tt) (inr true) tt x)) @
apD (PO_ind P l' r' pp') (colimp (inl tt) (inr false) tt x)^ = 
pp' x
    rewrite concat_p1, apD_V.
A, B, C: Type
f: A -> B
g: A -> C
P: PO f g -> Type
l': forall b : B, P (pol b)
r': forall c : C, P (por c)
pp': forall a : A, transport P (popp a) (l' (f a)) = r' (g a)
x: A
transport_pp P (colimp (inl tt) (inr true) tt x)
  (colimp (inl tt) (inr false) tt x)^ (PO_ind P l' r' pp' (pol (f x))) @
moveR_transport_V P (colimp (inl tt) (inr false) tt x)
  (PO_ind P l' r' pp' (colim (inl tt) x))
  (PO_ind P l' r' pp' (colim (inr false) (((span f g) _f tt) x)))
  (apD (PO_ind P l' r' pp') (colimp (inl tt) (inr false) tt x))^ =
pp' x
    rewrite (Colimit_ind_beta_colimp P _ _ (inl tt) (inr false) tt x).
A, B, C: Type
f: A -> B
g: A -> C
P: PO f g -> Type
l': forall b : B, P (pol b)
r': forall c : C, P (por c)
pp': forall a : A, transport P (popp a) (l' (f a)) = r' (g a)
x: A
transport_pp P (colimp (inl tt) (inr true) tt x)
  (colimp (inl tt) (inr false) tt x)^ (PO_ind P l' r' pp' (pol (f x))) @
moveR_transport_V P (colimp (inl tt) (inr false) tt x)
  (PO_ind P l' r' pp' (colim (inl tt) x))
  (PO_ind P l' r' pp' (colim (inr false) (((span f g) _f tt) x)))
  (PO_ind_arr P l' r' pp' (inl tt) (inr false) tt x)^ =
pp' x
    rewrite moveR_transport_p_V, moveR_moveL_transport_p.
A, B, C: Type
f: A -> B
g: A -> C
P: PO f g -> Type
l': forall b : B, P (pol b)
r': forall c : C, P (por c)
pp': forall a : A, transport P (popp a) (l' (f a)) = r' (g a)
x: A
transport_pp P (colimp (inl tt) (inr true) tt x)
  (colimp (inl tt) (inr false) tt x)^ (PO_ind P l' r' pp' (pol (f x))) @
((pp' x)^ @
 transport_pp P (colimp (inl tt) (inr true) tt x)
   (colimp (inl tt) (inr false) tt x)^ (l' (f x)))^ =
pp' x
    rewrite inv_pp, inv_V.
A, B, C: Type
f: A -> B
g: A -> C
P: PO f g -> Type
l': forall b : B, P (pol b)
r': forall c : C, P (por c)
pp': forall a : A, transport P (popp a) (l' (f a)) = r' (g a)
x: A
transport_pp P (colimp (inl tt) (inr true) tt x)
  (colimp (inl tt) (inr false) tt x)^ (PO_ind P l' r' pp' (pol (f x))) @
((transport_pp P (colimp (inl tt) (inr true) tt x)
    (colimp (inl tt) (inr false) tt x)^ (l' (f x)))^ @
 pp' x) =
pp' x
    apply concat_p_Vp.
  Defined.

  Definition PO_rec (P: Type) (l': B -> P) (r': C -> P)
    (pp': l' o f == r' o g) : PO f g -> P
    := Colimit_rec P (Build_span_cocone l' r' pp').

  Definition PO_rec_beta_pp (P: Type) (l': B -> P)
    (r': C -> P) (pp': l' o f == r' o g)
    : forall x, ap (PO_rec P l' r' pp') (popp x) = pp' x.
A, B, C: Type
f: A -> B
g: A -> C
P: Type
l': B -> P
r': C -> P
pp': l' o f == r' o g
forall x : A, ap (PO_rec P l' r' pp') (popp x) = pp' x
  Proof.
A, B, C: Type
f: A -> B
g: A -> C
P: Type
l': B -> P
r': C -> P
pp': l' o f == r' o g
forall x : A, ap (PO_rec P l' r' pp') (popp x) = pp' x
    intro x.
A, B, C: Type
f: A -> B
g: A -> C
P: Type
l': B -> P
r': C -> P
pp': l' o f == r' o g
x: A
ap (PO_rec P l' r' pp') (popp x) = pp' x
    unfold popp.
A, B, C: Type
f: A -> B
g: A -> C
P: Type
l': B -> P
r': C -> P
pp': l' o f == r' o g
x: A
ap (PO_rec P l' r' pp')
  (colimp (inl tt) (inr true) tt x @ (colimp (inl tt) (inr false) tt x)^) =
pp' x
    refine (ap_pp _ _ _ @ _ @ concat_p1 _).
A, B, C: Type
f: A -> B
g: A -> C
P: Type
l': B -> P
r': C -> P
pp': l' o f == r' o g
x: A
ap (PO_rec P l' r' pp') (colimp (inl tt) (inr true) tt x) @
ap (PO_rec P l' r' pp') (colimp (inl tt) (inr false) tt x)^ = 
pp' x @ 1
    refine (_ @@ _).
A, B, C: Type
f: A -> B
g: A -> C
P: Type
l': B -> P
r': C -> P
pp': l' o f == r' o g
x: A
ap (PO_rec P l' r' pp') (colimp (inl tt) (inr true) tt x) = pp' x
A, B, C: Type
f: A -> B
g: A -> C
P: Type
l': B -> P
r': C -> P
pp': l' o f == r' o g
x: A
ap (PO_rec P l' r' pp') (colimp (inl tt) (inr false) tt x)^ = 1
    1: exact (Colimit_rec_beta_colimp P (Build_span_cocone l' r' pp')
                (inl tt) (inr true) tt x).
A, B, C: Type
f: A -> B
g: A -> C
P: Type
l': B -> P
r': C -> P
pp': l' o f == r' o g
x: A
ap (PO_rec P l' r' pp') (colimp (inl tt) (inr false) tt x)^ = 1
    lhs napply ap_V.
A, B, C: Type
f: A -> B
g: A -> C
P: Type
l': B -> P
r': C -> P
pp': l' o f == r' o g
x: A
(ap (PO_rec P l' r' pp') (colimp (inl tt) (inr false) tt x))^ = 1
    apply (inverse2 (q:=1)).
A, B, C: Type
f: A -> B
g: A -> C
P: Type
l': B -> P
r': C -> P
pp': l' o f == r' o g
x: A
ap (PO_rec P l' r' pp') (colimp (inl tt) (inr false) tt x) = 1
    exact (Colimit_rec_beta_colimp P (Build_span_cocone l' r' pp')
             (inl tt) (inr false) tt x).
  Defined.

  (** A nice property: the pushout of an equivalence is an equivalence. *)
  #[export] Instance PO_of_equiv (Hf : IsEquiv f)
    : IsEquiv por.
A, B, C: Type
f: A -> B
g: A -> C
Hf: IsEquiv f
IsEquiv por
  Proof.
A, B, C: Type
f: A -> B
g: A -> C
Hf: IsEquiv f
IsEquiv por
    srapply isequiv_adjointify.
A, B, C: Type
f: A -> B
g: A -> C
Hf: IsEquiv f
PO f g -> C
A, B, C: Type
f: A -> B
g: A -> C
Hf: IsEquiv f
por o ?g == idmap
A, B, C: Type
f: A -> B
g: A -> C
Hf: IsEquiv f
?g o por == idmap
    -
A, B, C: Type
f: A -> B
g: A -> C
Hf: IsEquiv f
PO f g -> C srapply PO_rec.
A, B, C: Type
f: A -> B
g: A -> C
Hf: IsEquiv f
B -> C
A, B, C: Type
f: A -> B
g: A -> C
Hf: IsEquiv f
C -> C
A, B, C: Type
f: A -> B
g: A -> C
Hf: IsEquiv f
?l' o f == ?r' o g
      +
A, B, C: Type
f: A -> B
g: A -> C
Hf: IsEquiv f
B -> C exact (g o f^-1).
      +
A, B, C: Type
f: A -> B
g: A -> C
Hf: IsEquiv f
C -> C exact idmap.
      +
A, B, C: Type
f: A -> B
g: A -> C
Hf: IsEquiv f
g o f^-1 o f == idmap o g intro x.
A, B, C: Type
f: A -> B
g: A -> C
Hf: IsEquiv f
x: A
g (f^-1 (f x)) = g x
        apply ap, eissect.
    -
A, B, C: Type
f: A -> B
g: A -> C
Hf: IsEquiv f
por
o PO_rec C (g o f^-1) idmap
    ((fun x : A => ap g (eissect f x)) : g o f^-1 o f == idmap o g) ==
idmap srapply PO_ind; cbn.
A, B, C: Type
f: A -> B
g: A -> C
Hf: IsEquiv f
forall b : B,
por
  (PO_rec C (fun x : B => g (f^-1 x)) idmap (fun x : A => ap g (eissect f x))
     (pol b)) =
pol b
A, B, C: Type
f: A -> B
g: A -> C
Hf: IsEquiv f
forall c : C,
por
  (PO_rec C (fun x : B => g (f^-1 x)) idmap (fun x : A => ap g (eissect f x))
     (por c)) =
por c
A, B, C: Type
f: A -> B
g: A -> C
Hf: IsEquiv f
forall a : A,
transport
  (fun w : PO f g =>
   por
     (PO_rec C (fun x : B => g (f^-1 x)) idmap
        (fun x : A => ap g (eissect f x)) w) =
   w)
  (popp a) (?Goal (f a)) =
?Goal0 (g a)
      +
A, B, C: Type
f: A -> B
g: A -> C
Hf: IsEquiv f
forall b : B,
por
  (PO_rec C (fun x : B => g (f^-1 x)) idmap (fun x : A => ap g (eissect f x))
     (pol b)) =
pol b intro.
A, B, C: Type
f: A -> B
g: A -> C
Hf: IsEquiv f
b: B
por
  (PO_rec C (fun x : B => g (f^-1 x)) idmap (fun x : A => ap g (eissect f x))
     (pol b)) =
pol b
        refine ((popp _)^ @ _).
A, B, C: Type
f: A -> B
g: A -> C
Hf: IsEquiv f
b: B
pol (f (f^-1 b)) = pol b
        apply ap, eisretr.
      +
A, B, C: Type
f: A -> B
g: A -> C
Hf: IsEquiv f
forall c : C,
por
  (PO_rec C (fun x : B => g (f^-1 x)) idmap (fun x : A => ap g (eissect f x))
     (por c)) =
por c reflexivity.
      +
A, B, C: Type
f: A -> B
g: A -> C
Hf: IsEquiv f
forall a : A,
transport
  (fun w : PO f g =>
   por
     (PO_rec C (fun x : B => g (f^-1 x)) idmap
        (fun x : A => ap g (eissect f x)) w) =
   w)
  (popp a)
  ((fun b : B => (popp (f^-1 (inr true; b).2))^ @ ap pol (eisretr f b)) (f a)) =
(fun c : C => 1) (g a) intro a; cbn.
A, B, C: Type
f: A -> B
g: A -> C
Hf: IsEquiv f
a: A
transport
  (fun w : PO f g =>
   por
     (PO_rec C (fun x : B => g (f^-1 x)) idmap
        (fun x : A => ap g (eissect f x)) w) =
   w)
  (popp a) ((popp (f^-1 (f a)))^ @ ap pol (eisretr f (f a))) =
1
        transport_paths FFlr.
A, B, C: Type
f: A -> B
g: A -> C
Hf: IsEquiv f
a: A
ap por
  (ap
     (PO_rec C (fun x : B => g (f^-1 x)) idmap
        (fun x : A => ap g (eissect f x)))
     (popp a)) @
1 = ((popp (f^-1 (f a)))^ @ ap pol (eisretr f (f a))) @ popp a
        refine (concat_p1 _ @ _).
A, B, C: Type
f: A -> B
g: A -> C
Hf: IsEquiv f
a: A
ap por
  (ap
     (PO_rec C (fun x : B => g (f^-1 x)) idmap
        (fun x : A => ap g (eissect f x)))
     (popp a)) =
((popp (f^-1 (f a)))^ @ ap pol (eisretr f (f a))) @ popp a
        rewrite PO_rec_beta_pp.
A, B, C: Type
f: A -> B
g: A -> C
Hf: IsEquiv f
a: A
ap por (ap g (eissect f a)) =
((popp (f^-1 (f a)))^ @ ap pol (eisretr f (f a))) @ popp a
        rewrite eisadj.
A, B, C: Type
f: A -> B
g: A -> C
Hf: IsEquiv f
a: A
ap por (ap g (eissect f a)) =
((popp (f^-1 (f a)))^ @ ap pol (ap f (eissect f a))) @ popp a
        destruct (eissect f a); cbn.
A, B, C: Type
f: A -> B
g: A -> C
Hf: IsEquiv f
a: A
1 = ((popp (f^-1 (f a)))^ @ 1) @ popp (f^-1 (f a))
        rewrite concat_p1.
A, B, C: Type
f: A -> B
g: A -> C
Hf: IsEquiv f
a: A
1 = (popp (f^-1 (f a)))^ @ popp (f^-1 (f a))
        symmetry; apply concat_Vp.
    -
A, B, C: Type
f: A -> B
g: A -> C
Hf: IsEquiv f
PO_rec C (g o f^-1) idmap
  ((fun x : A => ap g (eissect f x)) : g o f^-1 o f == idmap o g)
o por == idmap cbn; reflexivity.
  Defined.

End PO.


(** ** Equivalence with [pushout] *)

Section is_PO_pushout.

  Import Colimits.Pushout.

  Context `{Funext} {A B C : Type} {f : A -> B} {g : A -> C}.

  Definition is_PO_pushout : is_PO f g (Pushout f g).
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
is_PO f g (Pushout f g)
  Proof.
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
is_PO f g (Pushout f g)
    srapply Build_IsColimit.
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
Cocone (span f g) (Pushout f g)
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
UniversalCocone ?C
    -
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
Cocone (span f g) (Pushout f g) srapply Build_span_cocone.
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
B -> Pushout f g
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
C -> Pushout f g
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
?inl' o f == ?inr' o g
      +
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
B -> Pushout f g exact (push o inl).
      +
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
C -> Pushout f g exact (push o inr).
      +
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
push o inl o f == push o inr o g exact pglue.
    -
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
UniversalCocone (Build_span_cocone (push o inl) (push o inr) pglue) srapply Build_UniversalCocone.
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
forall Y : Type,
IsEquiv
  (cocone_postcompose (Build_span_cocone (push o inl) (push o inr) pglue))
      intro Y; srapply isequiv_adjointify.
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
Y: Type
Cocone (span f g) Y -> Pushout f g -> Y
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
Y: Type
cocone_postcompose (Build_span_cocone (push o inl) (push o inr) pglue) o ?g ==
idmap
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
Y: Type
?g o cocone_postcompose (Build_span_cocone (push o inl) (push o inr) pglue) ==
idmap
      +
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
Y: Type
Cocone (span f g) Y -> Pushout f g -> Y intro Co.
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
Y: Type
Co: Cocone (span f g) Y
Pushout f g -> Y
        srapply Pushout_rec.
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
Y: Type
Co: Cocone (span f g) Y
B -> Y
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
Y: Type
Co: Cocone (span f g) Y
C -> Y
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
Y: Type
Co: Cocone (span f g) Y
forall a : A, ?pushb (f a) = ?pushc (g a)
        *
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
Y: Type
Co: Cocone (span f g) Y
B -> Y exact (pol' Co).
        *
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
Y: Type
Co: Cocone (span f g) Y
C -> Y exact (por' Co).
        *
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
Y: Type
Co: Cocone (span f g) Y
forall a : A, pol' Co (f a) = por' Co (g a) exact (popp' Co).
      +
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
Y: Type
cocone_postcompose (Build_span_cocone (push o inl) (push o inr) pglue)
o (fun Co : Cocone (span f g) Y =>
   Pushout_rec Y (pol' Co) (por' Co) (popp' Co)) ==
idmap intros [Co Co'].
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
Y: Type
Co: forall i : span_graph, span f g i -> Y
Co': forall (i j : span_graph) (g0 : span_graph i j),
(fun x : span f g i => Co j (((span f g) _f g0) x)) == Co i
cocone_postcompose
  (Build_span_cocone (fun x : B => push (inl x)) (fun x : C => push (inr x))
     pglue)
  (Pushout_rec Y (pol' {| legs := Co; legs_comm := Co' |})
     (por' {| legs := Co; legs_comm := Co' |})
     (popp' {| legs := Co; legs_comm := Co' |})) =
{| legs := Co; legs_comm := Co' |}
        srapply path_cocone.
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
Y: Type
Co: forall i : span_graph, span f g i -> Y
Co': forall (i j : span_graph) (g0 : span_graph i j),
(fun x : span f g i => Co j (((span f g) _f g0) x)) == Co i
forall i : span_graph,
cocone_postcompose
  (Build_span_cocone (fun x : B => push (inl x)) (fun x : C => push (inr x))
     pglue)
  (Pushout_rec Y (pol' {| legs := Co; legs_comm := Co' |})
     (por' {| legs := Co; legs_comm := Co' |})
     (popp' {| legs := Co; legs_comm := Co' |}))
  i ==
{| legs := Co; legs_comm := Co' |} i
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
Y: Type
Co: forall i : span_graph, span f g i -> Y
Co': forall (i j : span_graph) (g0 : span_graph i j),
(fun x : span f g i => Co j (((span f g) _f g0) x)) == Co i
forall (i j : span_graph) (g0 : span_graph i j) (x : span f g i),
legs_comm
  (cocone_postcompose
     (Build_span_cocone (fun x0 : B => push (inl x0))
        (fun x0 : C => push (inr x0)) pglue)
     (Pushout_rec Y (pol' {| legs := Co; legs_comm := Co' |})
        (por' {| legs := Co; legs_comm := Co' |})
        (popp' {| legs := Co; legs_comm := Co' |})))
  i j g0 x @
?path_legs i x =
?path_legs j (((span f g) _f g0) x) @
legs_comm {| legs := Co; legs_comm := Co' |} i j g0 x
        *
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
Y: Type
Co: forall i : span_graph, span f g i -> Y
Co': forall (i j : span_graph) (g0 : span_graph i j),
(fun x : span f g i => Co j (((span f g) _f g0) x)) == Co i
forall i : span_graph,
cocone_postcompose
  (Build_span_cocone (fun x : B => push (inl x)) (fun x : C => push (inr x))
     pglue)
  (Pushout_rec Y (pol' {| legs := Co; legs_comm := Co' |})
     (por' {| legs := Co; legs_comm := Co' |})
     (popp' {| legs := Co; legs_comm := Co' |}))
  i ==
{| legs := Co; legs_comm := Co' |} i intros [[]|[]] x; simpl.
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
Y: Type
Co: forall i : span_graph, span f g i -> Y
Co': forall (i j : span_graph) (g0 : span_graph i j),
(fun x0 : span f g i => Co j (((span f g) _f g0) x0)) == Co i
x: span f g (inl tt)
Co (inr false) (g x) = Co (inl tt) x
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
Y: Type
Co: forall i : span_graph, span f g i -> Y
Co': forall (i j : span_graph) (g0 : span_graph i j),
(fun x0 : span f g i => Co j (((span f g) _f g0) x0)) == Co i
x: span f g (inr true)
Co (inr true) x = Co (inr true) x
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
Y: Type
Co: forall i : span_graph, span f g i -> Y
Co': forall (i j : span_graph) (g0 : span_graph i j),
(fun x0 : span f g i => Co j (((span f g) _f g0) x0)) == Co i
x: span f g (inr false)
Co (inr false) x = Co (inr false) x
          1: apply (Co' (inl tt) (inr false) tt).
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
Y: Type
Co: forall i : span_graph, span f g i -> Y
Co': forall (i j : span_graph) (g0 : span_graph i j),
(fun x0 : span f g i => Co j (((span f g) _f g0) x0)) == Co i
x: span f g (inr true)
Co (inr true) x = Co (inr true) x
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
Y: Type
Co: forall i : span_graph, span f g i -> Y
Co': forall (i j : span_graph) (g0 : span_graph i j),
(fun x0 : span f g i => Co j (((span f g) _f g0) x0)) == Co i
x: span f g (inr false)
Co (inr false) x = Co (inr false) x
          all: reflexivity.
        *
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
Y: Type
Co: forall i : span_graph, span f g i -> Y
Co': forall (i j : span_graph) (g0 : span_graph i j),
(fun x : span f g i => Co j (((span f g) _f g0) x)) == Co i
forall (i j : span_graph) (g0 : span_graph i j) (x : span f g i),
legs_comm
  (cocone_postcompose
     (Build_span_cocone (fun x0 : B => push (inl x0))
        (fun x0 : C => push (inr x0)) pglue)
     (Pushout_rec Y (pol' {| legs := Co; legs_comm := Co' |})
        (por' {| legs := Co; legs_comm := Co' |})
        (popp' {| legs := Co; legs_comm := Co' |})))
  i j g0 x @
(fun i0 : span_graph =>
 match
   i0 as s
   return
     (cocone_postcompose
        (Build_span_cocone (fun x0 : B => push (inl x0))
           (fun x0 : C => push (inr x0)) pglue)
        (Pushout_rec Y (pol' {| legs := Co; legs_comm := Co' |})
           (por' {| legs := Co; legs_comm := Co' |})
           (popp' {| legs := Co; legs_comm := Co' |}))
        s ==
      {| legs := Co; legs_comm := Co' |} s)
 with
 | inl u =>
     (fun u0 : Unit =>
      match
        u0 as u1
        return
          (cocone_postcompose
             (Build_span_cocone (fun x0 : B => push (inl x0))
                (fun x0 : C => push (inr x0)) pglue)
             (Pushout_rec Y (pol' {| legs := Co; legs_comm := Co' |})
                (por' {| legs := Co; legs_comm := Co' |})
                (popp' {| legs := Co; legs_comm := Co' |}))
             (inl u1) ==
           {| legs := Co; legs_comm := Co' |} (inl u1))
      with
      | tt =>
          (fun x0 : span f g (inl tt) =>
           Co' (inl tt) (inr false) tt x0
           :
           cocone_postcompose
             (Build_span_cocone (fun x1 : B => push (inl x1))
                (fun x1 : C => push (inr x1)) pglue)
             (Pushout_rec Y (pol' {| legs := Co; legs_comm := Co' |})
                (por' {| legs := Co; legs_comm := Co' |})
                (popp' {| legs := Co; legs_comm := Co' |}))
             (inl tt) x0 =
           {| legs := Co; legs_comm := Co' |} (inl tt) x0)
          :
          cocone_postcompose
            (Build_span_cocone (fun x0 : B => push (inl x0))
               (fun x0 : C => push (inr x0)) pglue)
            (Pushout_rec Y (pol' {| legs := Co; legs_comm := Co' |})
               (por' {| legs := Co; legs_comm := Co' |})
               (popp' {| legs := Co; legs_comm := Co' |}))
            (inl tt) ==
          {| legs := Co; legs_comm := Co' |} (inl tt)
      end) u
 | inr b =>
     (fun b0 : Bool =>
      if b0 as b1
       return
         (cocone_postcompose
            (Build_span_cocone (fun x0 : B => push (inl x0))
               (fun x0 : C => push (inr x0)) pglue)
            (Pushout_rec Y (pol' {| legs := Co; legs_comm := Co' |})
               (por' {| legs := Co; legs_comm := Co' |})
               (popp' {| legs := Co; legs_comm := Co' |}))
            (inr b1) ==
          {| legs := Co; legs_comm := Co' |} (inr b1))
      then
       (fun x0 : span f g (inr true) =>
        1
        :
        cocone_postcompose
          (Build_span_cocone (fun x1 : B => push (inl x1))
             (fun x1 : C => push (inr x1)) pglue)
          (Pushout_rec Y (pol' {| legs := Co; legs_comm := Co' |})
             (por' {| legs := Co; legs_comm := Co' |})
             (popp' {| legs := Co; legs_comm := Co' |}))
          (inr true) x0 =
        {| legs := Co; legs_comm := Co' |} (inr true) x0)
       :
       cocone_postcompose
         (Build_span_cocone (fun x0 : B => push (inl x0))
            (fun x0 : C => push (inr x0)) pglue)
         (Pushout_rec Y (pol' {| legs := Co; legs_comm := Co' |})
            (por' {| legs := Co; legs_comm := Co' |})
            (popp' {| legs := Co; legs_comm := Co' |}))
         (inr true) ==
       {| legs := Co; legs_comm := Co' |} (inr true)
      else
       (fun x0 : span f g (inr false) =>
        1
        :
        cocone_postcompose
          (Build_span_cocone (fun x1 : B => push (inl x1))
             (fun x1 : C => push (inr x1)) pglue)
          (Pushout_rec Y (pol' {| legs := Co; legs_comm := Co' |})
             (por' {| legs := Co; legs_comm := Co' |})
             (popp' {| legs := Co; legs_comm := Co' |}))
          (inr false) x0 =
        {| legs := Co; legs_comm := Co' |} (inr false) x0)
       :
       cocone_postcompose
         (Build_span_cocone (fun x0 : B => push (inl x0))
            (fun x0 : C => push (inr x0)) pglue)
         (Pushout_rec Y (pol' {| legs := Co; legs_comm := Co' |})
            (por' {| legs := Co; legs_comm := Co' |})
            (popp' {| legs := Co; legs_comm := Co' |}))
         (inr false) ==
       {| legs := Co; legs_comm := Co' |} (inr false)) b
 end) i x =
(fun i0 : span_graph =>
 match
   i0 as s
   return
     (cocone_postcompose
        (Build_span_cocone (fun x0 : B => push (inl x0))
           (fun x0 : C => push (inr x0)) pglue)
        (Pushout_rec Y (pol' {| legs := Co; legs_comm := Co' |})
           (por' {| legs := Co; legs_comm := Co' |})
           (popp' {| legs := Co; legs_comm := Co' |}))
        s ==
      {| legs := Co; legs_comm := Co' |} s)
 with
 | inl u =>
     (fun u0 : Unit =>
      match
        u0 as u1
        return
          (cocone_postcompose
             (Build_span_cocone (fun x0 : B => push (inl x0))
                (fun x0 : C => push (inr x0)) pglue)
             (Pushout_rec Y (pol' {| legs := Co; legs_comm := Co' |})
                (por' {| legs := Co; legs_comm := Co' |})
                (popp' {| legs := Co; legs_comm := Co' |}))
             (inl u1) ==
           {| legs := Co; legs_comm := Co' |} (inl u1))
      with
      | tt =>
          (fun x0 : span f g (inl tt) =>
           Co' (inl tt) (inr false) tt x0
           :
           cocone_postcompose
             (Build_span_cocone (fun x1 : B => push (inl x1))
                (fun x1 : C => push (inr x1)) pglue)
             (Pushout_rec Y (pol' {| legs := Co; legs_comm := Co' |})
                (por' {| legs := Co; legs_comm := Co' |})
                (popp' {| legs := Co; legs_comm := Co' |}))
             (inl tt) x0 =
           {| legs := Co; legs_comm := Co' |} (inl tt) x0)
          :
          cocone_postcompose
            (Build_span_cocone (fun x0 : B => push (inl x0))
               (fun x0 : C => push (inr x0)) pglue)
            (Pushout_rec Y (pol' {| legs := Co; legs_comm := Co' |})
               (por' {| legs := Co; legs_comm := Co' |})
               (popp' {| legs := Co; legs_comm := Co' |}))
            (inl tt) ==
          {| legs := Co; legs_comm := Co' |} (inl tt)
      end) u
 | inr b =>
     (fun b0 : Bool =>
      if b0 as b1
       return
         (cocone_postcompose
            (Build_span_cocone (fun x0 : B => push (inl x0))
               (fun x0 : C => push (inr x0)) pglue)
            (Pushout_rec Y (pol' {| legs := Co; legs_comm := Co' |})
               (por' {| legs := Co; legs_comm := Co' |})
               (popp' {| legs := Co; legs_comm := Co' |}))
            (inr b1) ==
          {| legs := Co; legs_comm := Co' |} (inr b1))
      then
       (fun x0 : span f g (inr true) =>
        1
        :
        cocone_postcompose
          (Build_span_cocone (fun x1 : B => push (inl x1))
             (fun x1 : C => push (inr x1)) pglue)
          (Pushout_rec Y (pol' {| legs := Co; legs_comm := Co' |})
             (por' {| legs := Co; legs_comm := Co' |})
             (popp' {| legs := Co; legs_comm := Co' |}))
          (inr true) x0 =
        {| legs := Co; legs_comm := Co' |} (inr true) x0)
       :
       cocone_postcompose
         (Build_span_cocone (fun x0 : B => push (inl x0))
            (fun x0 : C => push (inr x0)) pglue)
         (Pushout_rec Y (pol' {| legs := Co; legs_comm := Co' |})
            (por' {| legs := Co; legs_comm := Co' |})
            (popp' {| legs := Co; legs_comm := Co' |}))
         (inr true) ==
       {| legs := Co; legs_comm := Co' |} (inr true)
      else
       (fun x0 : span f g (inr false) =>
        1
        :
        cocone_postcompose
          (Build_span_cocone (fun x1 : B => push (inl x1))
             (fun x1 : C => push (inr x1)) pglue)
          (Pushout_rec Y (pol' {| legs := Co; legs_comm := Co' |})
             (por' {| legs := Co; legs_comm := Co' |})
             (popp' {| legs := Co; legs_comm := Co' |}))
          (inr false) x0 =
        {| legs := Co; legs_comm := Co' |} (inr false) x0)
       :
       cocone_postcompose
         (Build_span_cocone (fun x0 : B => push (inl x0))
            (fun x0 : C => push (inr x0)) pglue)
         (Pushout_rec Y (pol' {| legs := Co; legs_comm := Co' |})
            (por' {| legs := Co; legs_comm := Co' |})
            (popp' {| legs := Co; legs_comm := Co' |}))
         (inr false) ==
       {| legs := Co; legs_comm := Co' |} (inr false)) b
 end) j (((span f g) _f g0) x) @
legs_comm {| legs := Co; legs_comm := Co' |} i j g0 x cbn beta.
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
Y: Type
Co: forall i : span_graph, span f g i -> Y
Co': forall (i j : span_graph) (g0 : span_graph i j),
(fun x : span f g i => Co j (((span f g) _f g0) x)) == Co i
forall (i j : span_graph) (g0 : span_graph i j) (x : span f g i),
legs_comm
  (cocone_postcompose
     (Build_span_cocone (fun x0 : B => push (inl x0))
        (fun x0 : C => push (inr x0)) pglue)
     (Pushout_rec Y (pol' {| legs := Co; legs_comm := Co' |})
        (por' {| legs := Co; legs_comm := Co' |})
        (popp' {| legs := Co; legs_comm := Co' |})))
  i j g0 x @
match
  i as s
  return
    (cocone_postcompose
       (Build_span_cocone (fun x0 : B => push (inl x0))
          (fun x0 : C => push (inr x0)) pglue)
       (Pushout_rec Y (pol' {| legs := Co; legs_comm := Co' |})
          (por' {| legs := Co; legs_comm := Co' |})
          (popp' {| legs := Co; legs_comm := Co' |}))
       s ==
     {| legs := Co; legs_comm := Co' |} s)
with
| inl u =>
    match
      u as u0
      return
        (cocone_postcompose
           (Build_span_cocone (fun x0 : B => push (inl x0))
              (fun x0 : C => push (inr x0)) pglue)
           (Pushout_rec Y (pol' {| legs := Co; legs_comm := Co' |})
              (por' {| legs := Co; legs_comm := Co' |})
              (popp' {| legs := Co; legs_comm := Co' |}))
           (inl u0) ==
         {| legs := Co; legs_comm := Co' |} (inl u0))
    with
    | tt => fun x0 : span f g (inl tt) => Co' (inl tt) (inr false) tt x0
    end
| inr b =>
    if b as b0
     return
       (cocone_postcompose
          (Build_span_cocone (fun x0 : B => push (inl x0))
             (fun x0 : C => push (inr x0)) pglue)
          (Pushout_rec Y (pol' {| legs := Co; legs_comm := Co' |})
             (por' {| legs := Co; legs_comm := Co' |})
             (popp' {| legs := Co; legs_comm := Co' |}))
          (inr b0) ==
        {| legs := Co; legs_comm := Co' |} (inr b0))
    then fun x0 : span f g (inr true) => 1
    else fun x0 : span f g (inr false) => 1
end x =
match
  j as s
  return
    (cocone_postcompose
       (Build_span_cocone (fun x0 : B => push (inl x0))
          (fun x0 : C => push (inr x0)) pglue)
       (Pushout_rec Y (pol' {| legs := Co; legs_comm := Co' |})
          (por' {| legs := Co; legs_comm := Co' |})
          (popp' {| legs := Co; legs_comm := Co' |}))
       s ==
     {| legs := Co; legs_comm := Co' |} s)
with
| inl u =>
    match
      u as u0
      return
        (cocone_postcompose
           (Build_span_cocone (fun x0 : B => push (inl x0))
              (fun x0 : C => push (inr x0)) pglue)
           (Pushout_rec Y (pol' {| legs := Co; legs_comm := Co' |})
              (por' {| legs := Co; legs_comm := Co' |})
              (popp' {| legs := Co; legs_comm := Co' |}))
           (inl u0) ==
         {| legs := Co; legs_comm := Co' |} (inl u0))
    with
    | tt => fun x0 : span f g (inl tt) => Co' (inl tt) (inr false) tt x0
    end
| inr b =>
    if b as b0
     return
       (cocone_postcompose
          (Build_span_cocone (fun x0 : B => push (inl x0))
             (fun x0 : C => push (inr x0)) pglue)
          (Pushout_rec Y (pol' {| legs := Co; legs_comm := Co' |})
             (por' {| legs := Co; legs_comm := Co' |})
             (popp' {| legs := Co; legs_comm := Co' |}))
          (inr b0) ==
        {| legs := Co; legs_comm := Co' |} (inr b0))
    then fun x0 : span f g (inr true) => 1
    else fun x0 : span f g (inr false) => 1
end (((span f g) _f g0) x) @
legs_comm {| legs := Co; legs_comm := Co' |} i j g0 x
          intros [u|b] [u'|b'] [] x.
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
Y: Type
Co: forall i : span_graph, span f g i -> Y
Co': forall (i j : span_graph) (g0 : span_graph i j),
(fun x0 : span f g i => Co j (((span f g) _f g0) x0)) == Co i
u: Unit
b': Bool
x: span f g (inl u)
legs_comm
  (cocone_postcompose
     (Build_span_cocone (fun x0 : B => push (inl x0))
        (fun x0 : C => push (inr x0)) pglue)
     (Pushout_rec Y (pol' {| legs := Co; legs_comm := Co' |})
        (por' {| legs := Co; legs_comm := Co' |})
        (popp' {| legs := Co; legs_comm := Co' |})))
  (inl u) (inr b') tt x @
match
  u as u0
  return
    (cocone_postcompose
       (Build_span_cocone (fun x0 : B => push (inl x0))
          (fun x0 : C => push (inr x0)) pglue)
       (Pushout_rec Y (pol' {| legs := Co; legs_comm := Co' |})
          (por' {| legs := Co; legs_comm := Co' |})
          (popp' {| legs := Co; legs_comm := Co' |}))
       (inl u0) ==
     {| legs := Co; legs_comm := Co' |} (inl u0))
with
| tt => fun x0 : span f g (inl tt) => Co' (inl tt) (inr false) tt x0
end x =
(if b' as b
  return
    (cocone_postcompose
       (Build_span_cocone (fun x0 : B => push (inl x0))
          (fun x0 : C => push (inr x0)) pglue)
       (Pushout_rec Y (pol' {| legs := Co; legs_comm := Co' |})
          (por' {| legs := Co; legs_comm := Co' |})
          (popp' {| legs := Co; legs_comm := Co' |}))
       (inr b) ==
     {| legs := Co; legs_comm := Co' |} (inr b))
 then fun x0 : span f g (inr true) => 1
 else fun x0 : span f g (inr false) => 1) (((span f g) _f tt) x) @
legs_comm {| legs := Co; legs_comm := Co' |} (inl u) (inr b') tt x
          destruct u, b'; cbn.
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
Y: Type
Co: forall i : span_graph, span f g i -> Y
Co': forall (i j : span_graph) (g0 : span_graph i j),
(fun x0 : span f g i => Co j (((span f g) _f g0) x0)) == Co i
x: span f g (inl tt)
ap
  (Pushout_rec Y (Co (inr true)) (Co (inr false))
     (popp' {| legs := Co; legs_comm := Co' |}))
  (pglue x) @
Co' (inl tt) (inr false) tt x = 1 @ Co' (inl tt) (inr true) tt x
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
Y: Type
Co: forall i : span_graph, span f g i -> Y
Co': forall (i j : span_graph) (g0 : span_graph i j),
(fun x0 : span f g i => Co j (((span f g) _f g0) x0)) == Co i
x: span f g (inl tt)
1 @ Co' (inl tt) (inr false) tt x = 1 @ Co' (inl tt) (inr false) tt x
          2: reflexivity.
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
Y: Type
Co: forall i : span_graph, span f g i -> Y
Co': forall (i j : span_graph) (g0 : span_graph i j),
(fun x0 : span f g i => Co j (((span f g) _f g0) x0)) == Co i
x: span f g (inl tt)
ap
  (Pushout_rec Y (Co (inr true)) (Co (inr false))
     (popp' {| legs := Co; legs_comm := Co' |}))
  (pglue x) @
Co' (inl tt) (inr false) tt x = 1 @ Co' (inl tt) (inr true) tt x
          rhs napply concat_1p.
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
Y: Type
Co: forall i : span_graph, span f g i -> Y
Co': forall (i j : span_graph) (g0 : span_graph i j),
(fun x0 : span f g i => Co j (((span f g) _f g0) x0)) == Co i
x: span f g (inl tt)
ap
  (Pushout_rec Y (Co (inr true)) (Co (inr false))
     (popp' {| legs := Co; legs_comm := Co' |}))
  (pglue x) @
Co' (inl tt) (inr false) tt x = Co' (inl tt) (inr true) tt x
          lhs refine (_ @@ 1).
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
Y: Type
Co: forall i : span_graph, span f g i -> Y
Co': forall (i j : span_graph) (g0 : span_graph i j),
(fun x0 : span f g i => Co j (((span f g) _f g0) x0)) == Co i
x: span f g (inl tt)
ap
  (Pushout_rec Y (Co (inr true)) (Co (inr false))
     (popp' {| legs := Co; legs_comm := Co' |}))
  (pglue x) =
?Goal
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
Y: Type
Co: forall i : span_graph, span f g i -> Y
Co': forall (i j : span_graph) (g0 : span_graph i j),
(fun x0 : span f g i => Co j (((span f g) _f g0) x0)) == Co i
x: span f g (inl tt)
?Goal @ Co' (inl tt) (inr false) tt x = Co' (inl tt) (inr true) tt x
          1: napply Pushout_rec_beta_pglue.
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
Y: Type
Co: forall i : span_graph, span f g i -> Y
Co': forall (i j : span_graph) (g0 : span_graph i j),
(fun x0 : span f g i => Co j (((span f g) _f g0) x0)) == Co i
x: span f g (inl tt)
popp' {| legs := Co; legs_comm := Co' |} x @ Co' (inl tt) (inr false) tt x =
Co' (inl tt) (inr true) tt x
          unfold popp', legs_comm.
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
Y: Type
Co: forall i : span_graph, span f g i -> Y
Co': forall (i j : span_graph) (g0 : span_graph i j),
(fun x0 : span f g i => Co j (((span f g) _f g0) x0)) == Co i
x: span f g (inl tt)
(Co' (inl tt) (inr true) tt x @ (Co' (inl tt) (inr false) tt x)^) @
Co' (inl tt) (inr false) tt x = Co' (inl tt) (inr true) tt x
          apply concat_pV_p.
      +
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
Y: Type
(fun Co : Cocone (span f g) Y => Pushout_rec Y (pol' Co) (por' Co) (popp' Co))
o cocone_postcompose (Build_span_cocone (push o inl) (push o inr) pglue) ==
idmap intro h.
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
Y: Type
h: Pushout f g -> Y
Pushout_rec Y
  (pol'
     (cocone_postcompose
        (Build_span_cocone (fun x : B => push (inl x))
           (fun x : C => push (inr x)) pglue)
        h))
  (por'
     (cocone_postcompose
        (Build_span_cocone (fun x : B => push (inl x))
           (fun x : C => push (inr x)) pglue)
        h))
  (popp'
     (cocone_postcompose
        (Build_span_cocone (fun x : B => push (inl x))
           (fun x : C => push (inr x)) pglue)
        h)) =
h
        apply path_forall.
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
Y: Type
h: Pushout f g -> Y
Pushout_rec Y
  (pol'
     (cocone_postcompose
        (Build_span_cocone (fun x : B => push (inl x))
           (fun x : C => push (inr x)) pglue)
        h))
  (por'
     (cocone_postcompose
        (Build_span_cocone (fun x : B => push (inl x))
           (fun x : C => push (inr x)) pglue)
        h))
  (popp'
     (cocone_postcompose
        (Build_span_cocone (fun x : B => push (inl x))
           (fun x : C => push (inr x)) pglue)
        h)) ==
h
        srapply Pushout_ind; cbn.
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
Y: Type
h: Pushout f g -> Y
forall b : B,
Pushout_rec Y (fun x : B => h (push (inl x))) (fun x : C => h (push (inr x)))
  (popp'
     (cocone_postcompose
        (Build_span_cocone (fun x : B => push (inl x))
           (fun x : C => push (inr x)) pglue)
        h))
  (pushl b) =
h (pushl b)
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
Y: Type
h: Pushout f g -> Y
forall c : C,
Pushout_rec Y (fun x : B => h (push (inl x))) (fun x : C => h (push (inr x)))
  (popp'
     (cocone_postcompose
        (Build_span_cocone (fun x : B => push (inl x))
           (fun x : C => push (inr x)) pglue)
        h))
  (pushr c) =
h (pushr c)
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
Y: Type
h: Pushout f g -> Y
forall a : A,
transport
  (fun w : Pushout f g =>
   Pushout_rec Y (fun x : B => h (push (inl x)))
     (fun x : C => h (push (inr x)))
     (popp'
        (cocone_postcompose
           (Build_span_cocone (fun x : B => push (inl x))
              (fun x : C => push (inr x)) pglue)
           h))
     w =
   h w)
  (pglue a) (?Goal (f a)) =
?Goal0 (g a)
        1,2: reflexivity.
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
Y: Type
h: Pushout f g -> Y
forall a : A,
transport
  (fun w : Pushout f g =>
   Pushout_rec Y (fun x : B => h (push (inl x)))
     (fun x : C => h (push (inr x)))
     (popp'
        (cocone_postcompose
           (Build_span_cocone (fun x : B => push (inl x))
              (fun x : C => push (inr x)) pglue)
           h))
     w =
   h w)
  (pglue a) ((fun b : B => 1) (f a)) =
(fun c : C => 1) (g a)
        intro a; cbn beta.
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
Y: Type
h: Pushout f g -> Y
a: A
transport
  (fun w : Pushout f g =>
   Pushout_rec Y (fun x : B => h (push (inl x)))
     (fun x : C => h (push (inr x)))
     (popp'
        (cocone_postcompose
           (Build_span_cocone (fun x : B => push (inl x))
              (fun x : C => push (inr x)) pglue)
           h))
     w =
   h w)
  (pglue a) 1 =
1
        transport_paths FlFr; apply equiv_p1_1q.
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
Y: Type
h: Pushout f g -> Y
a: A
ap
  (Pushout_rec Y (fun x : B => h (push (inl x)))
     (fun x : C => h (push (inr x)))
     (popp'
        (cocone_postcompose
           (Build_span_cocone (fun x : B => push (inl x))
              (fun x : C => push (inr x)) pglue)
           h)))
  (pglue a) =
ap h (pglue a)
        unfold popp'; cbn.
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
Y: Type
h: Pushout f g -> Y
a: A
ap
  (Pushout_rec Y (fun x : B => h (push (inl x)))
     (fun x : C => h (push (inr x))) (fun x : A => ap h (pglue x) @ 1))
  (pglue a) =
ap h (pglue a)
        rhs_V napply concat_p1.
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
Y: Type
h: Pushout f g -> Y
a: A
ap
  (Pushout_rec Y (fun x : B => h (push (inl x)))
     (fun x : C => h (push (inr x))) (fun x : A => ap h (pglue x) @ 1))
  (pglue a) =
ap h (pglue a) @ 1
        napply Pushout_rec_beta_pglue.
  Defined.

  Definition equiv_pushout_PO : Pushout f g <~> PO f g.
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
Pushout f g <~> PO f g
  Proof.
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
Pushout f g <~> PO f g
    srapply colimit_unicity.
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
Graph
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
Diagram ?G
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
IsColimit ?D (Pushout f g)
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
IsColimit ?D (PO f g)
    3: eapply is_PO_pushout.
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
IsColimit (span f g) (PO f g)
    eapply iscolimit_colimit.
  Defined.

  Definition equiv_pushout_PO_beta_pglue (a : A)
    : ap equiv_pushout_PO (pglue a) = popp a.
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
a: A
ap equiv_pushout_PO (pglue a) = popp a
  Proof.
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
a: A
ap equiv_pushout_PO (pglue a) = popp a
    cbn.
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
a: A
ap
  (Pushout_rec (PO f g) (fun x : B => colim (inr true) x)
     (fun x : C => colim (inr false) x)
     (popp'
        (cocone_precompose (diagram_idmap (span f g))
           (cocone_colimit (span f g)))))
  (pglue a) =
popp a
    refine (_ @ _).
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
a: A
ap
  (Pushout_rec (PO f g) (fun x : B => colim (inr true) x)
     (fun x : C => colim (inr false) x)
     (popp'
        (cocone_precompose (diagram_idmap (span f g))
           (cocone_colimit (span f g)))))
  (pglue a) =
?Goal
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
a: A
?Goal = popp a
    1: napply Pushout_rec_beta_pglue.
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
a: A
popp'
  (cocone_precompose (diagram_idmap (span f g)) (cocone_colimit (span f g)))
  a =
popp a
    unfold popp'; cbn.
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
a: A
(1 @ colimp (inl tt) (inr true) tt a) @
(1 @ colimp (inl tt) (inr false) tt a)^ = popp a
    rewrite 2 concat_1p.
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
a: A
colimp (inl tt) (inr true) tt a @ (colimp (inl tt) (inr false) tt a)^ =
popp a
    reflexivity.
  Defined.

  Definition Pushout_rec_PO_rec (P : Type) (pushb : B -> P) (pushc : C -> P)
    (pusha : forall a : A, pushb (f a) = pushc (g a))
    : Pushout_rec P pushb pushc pusha == PO_rec P pushb pushc pusha o equiv_pushout_PO.
H: Funext
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)
Pushout_rec P pushb pushc pusha ==
PO_rec P pushb pushc pusha o equiv_pushout_PO
  Proof.
H: Funext
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)
Pushout_rec P pushb pushc pusha ==
PO_rec P pushb pushc pusha o equiv_pushout_PO
    snapply Pushout_ind.
H: Funext
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)
forall b : B,
(fun w : Pushout f g =>
 Pushout_rec P pushb pushc pusha w =
 (PO_rec P pushb pushc pusha o equiv_pushout_PO) w) 
  (pushl b)
H: Funext
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)
forall c : C,
(fun w : Pushout f g =>
 Pushout_rec P pushb pushc pusha w =
 (PO_rec P pushb pushc pusha o equiv_pushout_PO) w) 
  (pushr c)
H: Funext
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)
forall a : A,
transport
  (fun w : Pushout f g =>
   Pushout_rec P pushb pushc pusha w =
   (PO_rec P pushb pushc pusha o equiv_pushout_PO) w)
  (pglue a) (?pushb (f a)) =
?pushc (g a)
    1, 2: 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, pushb (f a) = pushc (g a)
forall a : A,
transport
  (fun w : Pushout f g =>
   Pushout_rec P pushb pushc pusha w =
   (PO_rec P pushb pushc pusha o equiv_pushout_PO) w)
  (pglue a) ((fun b : B => 1) (f a)) =
(fun c : C => 1) (g a)
    intro a; cbn beta.
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
P: Type
pushb: B -> P
pushc: C -> P
pusha: forall a0 : A, pushb (f a0) = pushc (g a0)
a: A
transport
  (fun w : Pushout f g =>
   Pushout_rec P pushb pushc pusha w =
   PO_rec P pushb pushc pusha (equiv_pushout_PO w))
  (pglue a) 1 =
1
    transport_paths FlFr; apply equiv_p1_1q.
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
P: Type
pushb: B -> P
pushc: C -> P
pusha: forall a0 : A, pushb (f a0) = pushc (g a0)
a: A
ap (Pushout_rec P pushb pushc pusha) (pglue a) =
ap (fun x : Pushout f g => PO_rec P pushb pushc pusha (equiv_pushout_PO x))
  (pglue a)
    lhs exact (Pushout_rec_beta_pglue P pushb pushc pusha a).
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
P: Type
pushb: B -> P
pushc: C -> P
pusha: forall a0 : A, pushb (f a0) = pushc (g a0)
a: A
pusha a =
ap (fun x : Pushout f g => PO_rec P pushb pushc pusha (equiv_pushout_PO x))
  (pglue a)
    symmetry.
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
P: Type
pushb: B -> P
pushc: C -> P
pusha: forall a0 : A, pushb (f a0) = pushc (g a0)
a: A
ap (fun x : Pushout f g => PO_rec P pushb pushc pusha (equiv_pushout_PO x))
  (pglue a) =
pusha a
    lhs napply (ap_compose equiv_pushout_PO _ (pglue a)).
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
P: Type
pushb: B -> P
pushc: C -> P
pusha: forall a0 : A, pushb (f a0) = pushc (g a0)
a: A
ap (PO_rec P pushb pushc pusha) (ap equiv_pushout_PO (pglue a)) = pusha a
    lhs napply (ap _ (equiv_pushout_PO_beta_pglue a)).
H: Funext
A, B, C: Type
f: A -> B
g: A -> C
P: Type
pushb: B -> P
pushc: C -> P
pusha: forall a0 : A, pushb (f a0) = pushc (g a0)
a: A
ap (PO_rec P pushb pushc pusha) (popp a) = pusha a
    napply PO_rec_beta_pp.
  Defined.

End is_PO_pushout.