Colimit.v

Require Import Basics Types.[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Diagrams.Diagram.
Require Import Diagrams.Graph.
Require Import Diagrams.Cocone.
Require Import Diagrams.ConstantDiagram.
Require Import Diagrams.CommutativeSquares.
Require Import Colimits.Coeq.

Local Open Scope path_scope.
Generalizable All Variables.

(** This file contains the definition of colimits, and functoriality results on colimits. *)

(** * Colimits *)

(** ** Abstract definition *)

(** A colimit is the extremity of a cocone. *)
Class IsColimit `(D: Diagram G) (Q: Type) := {
  iscolimit_cocone :: Cocone D Q;
  iscolimit_unicocone : UniversalCocone iscolimit_cocone;
}.

Coercion iscolimit_cocone : IsColimit >-> Cocone.

Arguments Build_IsColimit {G D Q} C H : rename.
Arguments iscolimit_cocone {G D Q} C : rename.
Arguments iscolimit_unicocone {G D Q} H : rename.

(** [cocone_postcompose_inv] is defined for convenience: it is only the inverse of [cocone_postcompose]. It allows to recover the map [h] from a cocone [C']. *)

Definition cocone_postcompose_inv `{D: Diagram G} {Q X}
  (H : IsColimit D Q) (C' : Cocone D X) : Q -> X
  := @equiv_inv _ _ _ (iscolimit_unicocone H X) C'.

(** ** Existence of colimits *)

(** Every diagram has a colimit.  It could be described as the following HIT
<<
  HIT Colimit {G : Graph} (D : Diagram G) : Type :=
  | colim : forall i, D i -> Colimit D
  | colimp : forall i j (f : G i j) (x : D i) : colim j (D _f f x) = colim i x
  .
>>
but we instead describe it as the coequalizer of the source and target maps of the diagram.  The source type in the coequalizer ought to be:
<<
{x : sig D & {y : sig D & {f : G x.1 y.1 & D _f f x.2 = y.2}}}
>>
However we notice that the path type forms a contractible component, so we can use the more efficient:
<<
{x : sig D & {j : G & G x.1 j}}
>>
*)
Definition Colimit {G : Graph} (D : Diagram G) : Type :=
  @Coeq
    {x : sig D & {j : G & G x.1 j}}
    (sig D)
    (fun t => t.1)
    (fun t => (t.2.1; D _f t.2.2 t.1.2))
  .

Definition colim {G : Graph} {D : Diagram G} (i : G) (x : D i) : Colimit D :=
  coeq (i ; x).

Definition colimp {G : Graph} {D : Diagram G} (i j : G) (f : G i j) (x : D i)
  : colim j (D _f f x) = colim i x
  := (cglue ((i; x); j; f))^.

(** To obtain a path [colim j (D _f f x) = colim j (D _f f y)] from a path [x = y], one can either use [ap (D _f f)] followed by [ap (colim j)], or conjugate [ap (colim i)] by [colimp i j f]. These paths are equivalent. *)
Definition ap_colim_homotopic {G : Graph} {D : Diagram G} {i j : G} (f : G i j) {x y : D i} (p : x = y)
  : ap (colim j) (ap (D _f f) p)
    = colimp i j f x @ ap (colim i) p @ (colimp i j f y)^.G: Graph
D: Diagram G
i, j: G
f: G i j
x, y: D i
p: x = y
ap (colim j) (ap (D _f f) p) =
(colimp i j f x @ ap (colim i) p) @ (colimp i j f y)^
Proof.G: Graph
D: Diagram G
i, j: G
f: G i j
x, y: D i
p: x = y
ap (colim j) (ap (D _f f) p) =
(colimp i j f x @ ap (colim i) p) @ (colimp i j f y)^
  lhs_V napply ap_compose.G: Graph
D: Diagram G
i, j: G
f: G i j
x, y: D i
p: x = y
ap (fun x : D i => colim j ((D _f f) x)) p =
(colimp i j f x @ ap (colim i) p) @ (colimp i j f y)^
  exact (ap_homotopic (colimp _ _ _) p).
Defined.

Definition Colimit_ind {G : Graph} {D : Diagram G} (P : Colimit D -> Type)
(q : forall i x, P (colim i x))
(pp_q : forall (i j : G) (g: G i j) (x : D i),
  (@colimp G D i j g x) # (q j (D _f g x)) = q i x)
: forall w, P w.G: Graph
D: Diagram G
P: Colimit D -> Type
q: forall (i : G) (x : D i), P (colim i x)
pp_q: forall (i j : G) (g : G i j) 
(x : D i),
transport P (colimp i j g x) (q j ((D _f g) x)) =
q i x
forall w : Colimit D, P w
Proof.G: Graph
D: Diagram G
P: Colimit D -> Type
q: forall (i : G) (x : D i), P (colim i x)
pp_q: forall (i j : G) (g : G i j) 
(x : D i),
transport P (colimp i j g x) (q j ((D _f g) x)) =
q i x
forall w : Colimit D, P w
  srapply Coeq_ind.G: Graph
D: Diagram G
P: Colimit D -> Type
q: forall (i : G) (x : D i), P (colim i x)
pp_q: forall (i j : G) (g : G i j) 
(x : D i),
transport P (colimp i j g x) (q j ((D _f g) x)) =
q i x
forall a : {x : _ & D x}, P (coeq a)
G: Graph
D: Diagram G
P: Colimit D -> Type
q: forall (i : G) (x : D i), P (colim i x)
pp_q: forall (i j : G) (g : G i j) 
(x : D i),
transport P (colimp i j g x) (q j ((D _f g) x)) =
q i x
forall b : {x : {x : _ & D x} & {j : G & G x.1 j}},
transport P (cglue b)
  (?coeq'
     ((fun t : {x : {x : _ & D x} & {j : G & G x.1 j}}
       => t.1) b)) =
?coeq'
  ((fun t : {x : {x : _ & D x} & {j : G & G x.1 j}} =>
    ((t.2).1; (D _f (t.2).2) (t.1).2)) b)
  -G: Graph
D: Diagram G
P: Colimit D -> Type
q: forall (i : G) (x : D i), P (colim i x)
pp_q: forall (i j : G) (g : G i j) 
(x : D i),
transport P (colimp i j g x) (q j ((D _f g) x)) =
q i x
forall a : {x : _ & D x}, P (coeq a) intros [x i].G: Graph
D: Diagram G
P: Colimit D -> Type
q: forall (i : G) (x : D i), P (colim i x)
pp_q: forall (i j : G) (g : G i j) 
(x : D i),
transport P (colimp i j g x) (q j ((D _f g) x)) =
q i x
x: G
i: D x
P (coeq (x; i))
    exact (q x i).
  -G: Graph
D: Diagram G
P: Colimit D -> Type
q: forall (i : G) (x : D i), P (colim i x)
pp_q: forall (i j : G) (g : G i j) 
(x : D i),
transport P (colimp i j g x) (q j ((D _f g) x)) =
q i x
forall b : {x : {x : _ & D x} & {j : G & G x.1 j}},
transport P (cglue b)
  ((fun a : {x : _ & D x} =>
    (fun (x : G) (i : D x) => q x i) a.1 a.2)
     ((fun t : {x : {x : _ & D x} & {j : G & G x.1 j}}
       => t.1) b)) =
(fun a : {x : _ & D x} =>
 (fun (x : G) (i : D x) => q x i) a.1 a.2)
  ((fun t : {x : {x : _ & D x} & {j : G & G x.1 j}} =>
    ((t.2).1; (D _f (t.2).2) (t.1).2)) b) intros [[i x] [j f]].G: Graph
D: Diagram G
P: Colimit D -> Type
q: forall (i : G) (x : D i), P (colim i x)
pp_q: forall (i j : G) (g : G i j) 
(x : D i),
transport P (colimp i j g x) (q j ((D _f g) x)) =
q i x
i: G
x: D i
j: G
f: G (i; x).1 j
transport P (cglue ((i; x); j; f))
  (q (((i; x); j; f).1).1 (((i; x); j; f).1).2) =
q (((i; x); j; f).2).1
  ((D _f (((i; x); j; f).2).2) (((i; x); j; f).1).2)
    cbn in f; cbn.G: Graph
D: Diagram G
P: Colimit D -> Type
q: forall (i : G) (x : D i), P (colim i x)
pp_q: forall (i j : G) (g : G i j) 
(x : D i),
transport P (colimp i j g x) (q j ((D _f g) x)) =
q i x
i: G
x: D i
j: G
f: G i j
transport P (cglue ((i; x); j; f)) (q i x) =
q j ((D _f f) x)
    apply moveR_transport_p.G: Graph
D: Diagram G
P: Colimit D -> Type
q: forall (i : G) (x : D i), P (colim i x)
pp_q: forall (i j : G) (g : G i j) 
(x : D i),
transport P (colimp i j g x) (q j ((D _f g) x)) =
q i x
i: G
x: D i
j: G
f: G i j
q i x =
transport P (cglue ((i; x); j; f))^ (q j ((D _f f) x))
    symmetry.G: Graph
D: Diagram G
P: Colimit D -> Type
q: forall (i : G) (x : D i), P (colim i x)
pp_q: forall (i j : G) (g : G i j) 
(x : D i),
transport P (colimp i j g x) (q j ((D _f g) x)) =
q i x
i: G
x: D i
j: G
f: G i j
transport P (cglue ((i; x); j; f))^ (q j ((D _f f) x)) =
q i x
    exact (pp_q _ _ _ _).
Defined.

Definition Colimit_ind_beta_colimp {G : Graph} {D : Diagram G}
  (P : Colimit D -> Type) (q : forall i x, P (colim i x))
  (pp_q : forall (i j: G) (g: G i j) (x: D i),
    @colimp G D i j g x # q _ (D _f g x) = q _ x)
  (i j : G) (g : G i j) (x : D i)
  : apD (Colimit_ind P q pp_q) (colimp i j g x) = pp_q i j g x.G: Graph
D: Diagram G
P: Colimit D -> Type
q: forall (i : G) (x : D i), P (colim i x)
pp_q: forall (i j : G) (g : G i j) 
(x : D i),
transport P (colimp i j g x) (q j ((D _f g) x)) =
q i x
i, j: G
g: G i j
x: D i
apD (Colimit_ind P q pp_q) (colimp i j g x) =
pp_q i j g x
Proof.G: Graph
D: Diagram G
P: Colimit D -> Type
q: forall (i : G) (x : D i), P (colim i x)
pp_q: forall (i j : G) (g : G i j) 
(x : D i),
transport P (colimp i j g x) (q j ((D _f g) x)) =
q i x
i, j: G
g: G i j
x: D i
apD (Colimit_ind P q pp_q) (colimp i j g x) =
pp_q i j g x
  refine (apD_V _ _ @ _).G: Graph
D: Diagram G
P: Colimit D -> Type
q: forall (i : G) (x : D i), P (colim i x)
pp_q: forall (i j : G) (g : G i j) 
(x : D i),
transport P (colimp i j g x) (q j ((D _f g) x)) =
q i x
i, j: G
g: G i j
x: D i
moveR_transport_V P (cglue ((i; x); j; g))
  (Colimit_ind P q pp_q (colim j ((D _f g) x)))
  (Colimit_ind P q pp_q (colim i x))
  (apD (Colimit_ind P q pp_q) (cglue ((i; x); j; g)))^ =
pp_q i j g x
  apply moveR_equiv_M.G: Graph
D: Diagram G
P: Colimit D -> Type
q: forall (i : G) (x : D i), P (colim i x)
pp_q: forall (i j : G) (g : G i j) 
(x : D i),
transport P (colimp i j g x) (q j ((D _f g) x)) =
q i x
i, j: G
g: G i j
x: D i
(apD (Colimit_ind P q pp_q) (cglue ((i; x); j; g)))^ =
(moveR_transport_V P (cglue ((i; x); j; g))
   (Colimit_ind P q pp_q (colim j ((D _f g) x)))
   (Colimit_ind P q pp_q (colim i x)))^-1
  (pp_q i j g x)
  apply moveR_equiv_M.G: Graph
D: Diagram G
P: Colimit D -> Type
q: forall (i : G) (x : D i), P (colim i x)
pp_q: forall (i j : G) (g : G i j) 
(x : D i),
transport P (colimp i j g x) (q j ((D _f g) x)) =
q i x
i, j: G
g: G i j
x: D i
apD (Colimit_ind P q pp_q) (cglue ((i; x); j; g)) =
inverse^-1
  ((moveR_transport_V P (cglue ((i; x); j; g))
      (Colimit_ind P q pp_q (colim j ((D _f g) x)))
      (Colimit_ind P q pp_q (colim i x)))^-1
     (pp_q i j g x))
  refine (Coeq_ind_beta_cglue _ _ _ _ @ _).G: Graph
D: Diagram G
P: Colimit D -> Type
q: forall (i : G) (x : D i), P (colim i x)
pp_q: forall (i j : G) (g : G i j) 
(x : D i),
transport P (colimp i j g x) (q j ((D _f g) x)) =
q i x
i, j: G
g: G i j
x: D i
moveR_transport_p P (cglue ((i; x); j; g)) (q i x)
  (q j ((D _f g) x)) (pp_q i j g x)^ =
inverse^-1
  ((moveR_transport_V P (cglue ((i; x); j; g))
      (Colimit_ind P q pp_q (colim j ((D _f g) x)))
      (Colimit_ind P q pp_q (colim i x)))^-1
     (pp_q i j g x))
  symmetry.G: Graph
D: Diagram G
P: Colimit D -> Type
q: forall (i : G) (x : D i), P (colim i x)
pp_q: forall (i j : G) (g : G i j) 
(x : D i),
transport P (colimp i j g x) (q j ((D _f g) x)) =
q i x
i, j: G
g: G i j
x: D i
inverse^-1
  ((moveR_transport_V P (cglue ((i; x); j; g))
      (Colimit_ind P q pp_q (colim j ((D _f g) x)))
      (Colimit_ind P q pp_q (colim i x)))^-1
     (pp_q i j g x)) =
moveR_transport_p P (cglue ((i; x); j; g)) (q i x)
  (q j ((D _f g) x)) (pp_q i j g x)^
  apply moveL_transport_p_V.
Defined.

Definition Colimit_rec {G : Graph} {D : Diagram G} (P : Type) (C : Cocone D P)
  : Colimit D -> P.G: Graph
D: Diagram G
P: Type
C: Cocone D P
Colimit D -> P
Proof.G: Graph
D: Diagram G
P: Type
C: Cocone D P
Colimit D -> P
  srapply (Colimit_ind _ C).G: Graph
D: Diagram G
P: Type
C: Cocone D P
forall (i j : G) (g : G i j) (x : D i),
transport (fun _ : Colimit D => P) (colimp i j g x)
  (C j ((D _f g) x)) = C i x
  intros i j g x.G: Graph
D: Diagram G
P: Type
C: Cocone D P
i, j: G
g: G i j
x: D i
transport (fun _ : Colimit D => P) (colimp i j g x)
  (C j ((D _f g) x)) = C i x
  refine (transport_const _ _ @ _).G: Graph
D: Diagram G
P: Type
C: Cocone D P
i, j: G
g: G i j
x: D i
C j ((D _f g) x) = C i x
  apply legs_comm.
Defined.

Definition Colimit_rec_beta_colimp {G : Graph} {D : Diagram G}
  (P : Type) (C : Cocone D P) (i j : G) (g: G i j) (x: D i)
  : ap (Colimit_rec P C) (colimp i j g x) = legs_comm C i j g x.G: Graph
D: Diagram G
P: Type
C: Cocone D P
i, j: G
g: G i j
x: D i
ap (Colimit_rec P C) (colimp i j g x) =
legs_comm C i j g x
Proof.G: Graph
D: Diagram G
P: Type
C: Cocone D P
i, j: G
g: G i j
x: D i
ap (Colimit_rec P C) (colimp i j g x) =
legs_comm C i j g x
  rapply (cancelL (transport_const (colimp i j g x) _)).G: Graph
D: Diagram G
P: Type
C: Cocone D P
i, j: G
g: G i j
x: D i
transport_const (colimp i j g x)
  (Colimit_rec P C (colim j ((D _f g) x))) @
ap (Colimit_rec P C) (colimp i j g x) =
transport_const (colimp i j g x)
  (Colimit_rec P C (colim j ((D _f g) x))) @
legs_comm C i j g x
  srapply ((apD_const (Colimit_ind (fun _ => P) C _) (colimp i j g x))^ @ _).G: Graph
D: Diagram G
P: Type
C: Cocone D P
i, j: G
g: G i j
x: D i
apD
  (Colimit_ind (fun _ : Colimit D => P) C
     (fun (i j : G) (g : G i j) (x : D i) =>
      transport_const (colimp i j g x)
        (C j ((D _f g) x)) @ legs_comm C i j g x))
  (colimp i j g x) =
transport_const (colimp i j g x)
  (Colimit_rec P C (colim j ((D _f g) x))) @
legs_comm C i j g x
  exact (Colimit_ind_beta_colimp (fun _ => P) C _ i j g x).
Defined.

Arguments colim : simpl never.
Arguments colimp : simpl never.

(** The natural cocone to the colimit. *)
Definition cocone_colimit {G : Graph} (D : Diagram G) : Cocone D (Colimit D)
  := Build_Cocone colim colimp.

(** Given a cocone [C] and [f : Colimit D -> P] inducing a "homotopic" cocone, [Colimit_rec P C] is homotopic to [f]. *)
Definition Colimit_rec_homotopy {G : Graph} {D : Diagram G} (P : Type) (C : Cocone D P)
  (f : Colimit D -> P)
  (h_obj : forall i, legs C i == f o colim i)
  (h_comm : forall i j (g : G i j) x,
      legs_comm C i j g x @ h_obj i x = h_obj j ((D _f g) x) @ ap f (colimp i j g x))
  : Colimit_rec P C == f.G: Graph
D: Diagram G
P: Type
C: Cocone D P
f: Colimit D -> P
h_obj: forall i : G, C i == f o colim i
h_comm: forall (i j : G) (g : G i j) 
(x : D i),
legs_comm C i j g x @ h_obj i x =
h_obj j ((D _f g) x) @ ap f (colimp i j g x)
Colimit_rec P C == f
Proof.G: Graph
D: Diagram G
P: Type
C: Cocone D P
f: Colimit D -> P
h_obj: forall i : G, C i == f o colim i
h_comm: forall (i j : G) (g : G i j) 
(x : D i),
legs_comm C i j g x @ h_obj i x =
h_obj j ((D _f g) x) @ ap f (colimp i j g x)
Colimit_rec P C == f
  snapply Colimit_ind.G: Graph
D: Diagram G
P: Type
C: Cocone D P
f: Colimit D -> P
h_obj: forall i : G, C i == f o colim i
h_comm: forall (i j : G) (g : G i j) 
(x : D i),
legs_comm C i j g x @ h_obj i x =
h_obj j ((D _f g) x) @ ap f (colimp i j g x)
forall (i : G) (x : D i),
(fun w : Colimit D => Colimit_rec P C w = f w)
  (colim i x)
G: Graph
D: Diagram G
P: Type
C: Cocone D P
f: Colimit D -> P
h_obj: forall i : G, C i == f o colim i
h_comm: forall (i j : G) (g : G i j) 
(x : D i),
legs_comm C i j g x @ h_obj i x =
h_obj j ((D _f g) x) @ ap f (colimp i j g x)
forall (i j : G) (g : G i j) 
(x : D i),
transport
  (fun w : Colimit D => Colimit_rec P C w = f w)
  (colimp i j g x) (?q j ((D _f g) x)) = 
?q i x
  -G: Graph
D: Diagram G
P: Type
C: Cocone D P
f: Colimit D -> P
h_obj: forall i : G, C i == f o colim i
h_comm: forall (i j : G) (g : G i j) 
(x : D i),
legs_comm C i j g x @ h_obj i x =
h_obj j ((D _f g) x) @ ap f (colimp i j g x)
forall (i : G) (x : D i),
(fun w : Colimit D => Colimit_rec P C w = f w)
  (colim i x) simpl.G: Graph
D: Diagram G
P: Type
C: Cocone D P
f: Colimit D -> P
h_obj: forall i : G, C i == f o colim i
h_comm: forall (i j : G) (g : G i j) 
(x : D i),
legs_comm C i j g x @ h_obj i x =
h_obj j ((D _f g) x) @ ap f (colimp i j g x)
forall (i : G) (x : D i), C i x = f (colim i x) exact h_obj.
  -G: Graph
D: Diagram G
P: Type
C: Cocone D P
f: Colimit D -> P
h_obj: forall i : G, C i == f o colim i
h_comm: forall (i j : G) (g : G i j) 
(x : D i),
legs_comm C i j g x @ h_obj i x =
h_obj j ((D _f g) x) @ ap f (colimp i j g x)
forall (i j : G) (g : G i j) (x : D i),
transport
  (fun w : Colimit D => Colimit_rec P C w = f w)
  (colimp i j g x)
  ((h_obj
    :
    forall (i0 : G) (x0 : D i0),
    (fun w : Colimit D => Colimit_rec P C w = f w)
      (colim i0 x0)) j ((D _f g) x)) =
(h_obj
 :
 forall (i0 : G) (x0 : D i0),
 (fun w : Colimit D => Colimit_rec P C w = f w)
   (colim i0 x0)) i x cbn beta; intros i j g x.G: Graph
D: Diagram G
P: Type
C: Cocone D P
f: Colimit D -> P
h_obj: forall i : G, C i == f o colim i
h_comm: forall (i j : G) (g : G i j) 
(x : D i),
legs_comm C i j g x @ h_obj i x =
h_obj j ((D _f g) x) @ ap f (colimp i j g x)
i, j: G
g: G i j
x: D i
transport
  (fun w : Colimit D => Colimit_rec P C w = f w)
  (colimp i j g x) (h_obj j ((D _f g) x)) = h_obj i x
    transport_paths FlFr.G: Graph
D: Diagram G
P: Type
C: Cocone D P
f: Colimit D -> P
h_obj: forall i : G, C i == f o colim i
h_comm: forall (i j : G) (g : G i j) 
(x : D i),
legs_comm C i j g x @ h_obj i x =
h_obj j ((D _f g) x) @ ap f (colimp i j g x)
i, j: G
g: G i j
x: D i
ap (Colimit_rec P C) (colimp i j g x) @ h_obj i x =
h_obj j ((D _f g) x) @ ap f (colimp i j g x)
    lhs napply (Colimit_rec_beta_colimp _ _ _ _ _ _ @@ 1).G: Graph
D: Diagram G
P: Type
C: Cocone D P
f: Colimit D -> P
h_obj: forall i : G, C i == f o colim i
h_comm: forall (i j : G) (g : G i j) 
(x : D i),
legs_comm C i j g x @ h_obj i x =
h_obj j ((D _f g) x) @ ap f (colimp i j g x)
i, j: G
g: G i j
x: D i
legs_comm C i j g x @ h_obj i x =
h_obj j ((D _f g) x) @ ap f (colimp i j g x)
    apply h_comm.
Defined.

(** "Homotopic" cocones induces homotopic maps. *)
Definition Colimit_rec_homotopy' {G : Graph} {D : Diagram G} (P : Type) (C1 C2 : Cocone D P)
  (h_obj : forall i, legs C1 i == legs C2 i)
  (h_comm : forall i j (g : G i j) x,
      legs_comm C1 i j g x @ h_obj i x = h_obj j (D _f g x) @ legs_comm C2 i j g x)
  : Colimit_rec P C1 == Colimit_rec P C2.G: Graph
D: Diagram G
P: Type
C1, C2: Cocone D P
h_obj: forall i : G, C1 i == C2 i
h_comm: forall (i j : G) (g : G i j) 
(x : D i),
legs_comm C1 i j g x @ h_obj i x =
h_obj j ((D _f g) x) @ legs_comm C2 i j g x
Colimit_rec P C1 == Colimit_rec P C2
Proof.G: Graph
D: Diagram G
P: Type
C1, C2: Cocone D P
h_obj: forall i : G, C1 i == C2 i
h_comm: forall (i j : G) (g : G i j) 
(x : D i),
legs_comm C1 i j g x @ h_obj i x =
h_obj j ((D _f g) x) @ legs_comm C2 i j g x
Colimit_rec P C1 == Colimit_rec P C2
  snapply Colimit_rec_homotopy.G: Graph
D: Diagram G
P: Type
C1, C2: Cocone D P
h_obj: forall i : G, C1 i == C2 i
h_comm: forall (i j : G) (g : G i j) 
(x : D i),
legs_comm C1 i j g x @ h_obj i x =
h_obj j ((D _f g) x) @ legs_comm C2 i j g x
forall i : G, C1 i == Colimit_rec P C2 o colim i
G: Graph
D: Diagram G
P: Type
C1, C2: Cocone D P
h_obj: forall i : G, C1 i == C2 i
h_comm: forall (i j : G) (g : G i j) 
(x : D i),
legs_comm C1 i j g x @ h_obj i x =
h_obj j ((D _f g) x) @ legs_comm C2 i j g x
forall (i j : G) (g : G i j) 
(x : D i),
legs_comm C1 i j g x @ ?h_obj i x =
?h_obj j ((D _f g) x) @
ap (Colimit_rec P C2) (colimp i j g x)
  -G: Graph
D: Diagram G
P: Type
C1, C2: Cocone D P
h_obj: forall i : G, C1 i == C2 i
h_comm: forall (i j : G) (g : G i j) 
(x : D i),
legs_comm C1 i j g x @ h_obj i x =
h_obj j ((D _f g) x) @ legs_comm C2 i j g x
forall i : G, C1 i == Colimit_rec P C2 o colim i exact h_obj.
  -G: Graph
D: Diagram G
P: Type
C1, C2: Cocone D P
h_obj: forall i : G, C1 i == C2 i
h_comm: forall (i j : G) (g : G i j) 
(x : D i),
legs_comm C1 i j g x @ h_obj i x =
h_obj j ((D _f g) x) @ legs_comm C2 i j g x
forall (i j : G) (g : G i j) (x : D i),
legs_comm C1 i j g x @ h_obj i x =
h_obj j ((D _f g) x) @
ap (Colimit_rec P C2) (colimp i j g x) intros i j g x.G: Graph
D: Diagram G
P: Type
C1, C2: Cocone D P
h_obj: forall i : G, C1 i == C2 i
h_comm: forall (i j : G) (g : G i j) 
(x : D i),
legs_comm C1 i j g x @ h_obj i x =
h_obj j ((D _f g) x) @ legs_comm C2 i j g x
i, j: G
g: G i j
x: D i
legs_comm C1 i j g x @ h_obj i x =
h_obj j ((D _f g) x) @
ap (Colimit_rec P C2) (colimp i j g x)
    rhs napply (1 @@ Colimit_rec_beta_colimp _ _ _ _ _ _).G: Graph
D: Diagram G
P: Type
C1, C2: Cocone D P
h_obj: forall i : G, C1 i == C2 i
h_comm: forall (i j : G) (g : G i j) 
(x : D i),
legs_comm C1 i j g x @ h_obj i x =
h_obj j ((D _f g) x) @ legs_comm C2 i j g x
i, j: G
g: G i j
x: D i
legs_comm C1 i j g x @ h_obj i x =
h_obj j ((D _f g) x) @ legs_comm C2 i j g x
    apply h_comm.
Defined.

(** [Colimit_rec] is an equivalence. *)
Instance isequiv_colimit_rec `{Funext} {G : Graph}
  {D : Diagram G} (P : Type)
  : IsEquiv (Colimit_rec (D:=D) P).H: Funext
G: Graph
D: Diagram G
P: Type
IsEquiv (Colimit_rec P)
Proof.H: Funext
G: Graph
D: Diagram G
P: Type
IsEquiv (Colimit_rec P)
  srapply isequiv_adjointify.H: Funext
G: Graph
D: Diagram G
P: Type
(Colimit D -> P) -> Cocone D P
H: Funext
G: Graph
D: Diagram G
P: Type
Colimit_rec P o ?g == idmap
H: Funext
G: Graph
D: Diagram G
P: Type
?g o Colimit_rec P == idmap
  -H: Funext
G: Graph
D: Diagram G
P: Type
(Colimit D -> P) -> Cocone D P exact (cocone_postcompose (cocone_colimit D)).
  -H: Funext
G: Graph
D: Diagram G
P: Type
Colimit_rec P o cocone_postcompose (cocone_colimit D) ==
idmap intro f.H: Funext
G: Graph
D: Diagram G
P: Type
f: Colimit D -> P
Colimit_rec P
  (cocone_postcompose (cocone_colimit D) f) = f
    apply path_forall.H: Funext
G: Graph
D: Diagram G
P: Type
f: Colimit D -> P
Colimit_rec P
  (cocone_postcompose (cocone_colimit D) f) == f
    snapply Colimit_rec_homotopy.H: Funext
G: Graph
D: Diagram G
P: Type
f: Colimit D -> P
forall i : G,
cocone_postcompose (cocone_colimit D) f i ==
f o colim i
H: Funext
G: Graph
D: Diagram G
P: Type
f: Colimit D -> P
forall (i j : G) (g : G i j) (x : D i),
legs_comm (cocone_postcompose (cocone_colimit D) f) i
  j g x @ ?h_obj i x =
?h_obj j ((D _f g) x) @ ap f (colimp i j g x)
    1: reflexivity.H: Funext
G: Graph
D: Diagram G
P: Type
f: Colimit D -> P
forall (i j : G) (g : G i j) (x : D i),
legs_comm (cocone_postcompose (cocone_colimit D) f) i
  j g x @ (fun (i0 : G) (x0 : D i0) => 1) i x =
(fun (i0 : G) (x0 : D i0) => 1) j ((D _f g) x) @
ap f (colimp i j g x)
    intros; cbn.H: Funext
G: Graph
D: Diagram G
P: Type
f: Colimit D -> P
i, j: G
g: G i j
x: D i
ap f (colimp i j g x) @ 1 = 1 @ ap f (colimp i j g x)
    apply concat_p1_1p.
  -H: Funext
G: Graph
D: Diagram G
P: Type
cocone_postcompose (cocone_colimit D) o Colimit_rec P ==
idmap intros [].H: Funext
G: Graph
D: Diagram G
P: Type
legs: forall i : G, D i -> P
legs_comm: forall (i j : G) (g : G i j),
(fun x : D i => legs j ((D _f g) x)) ==
legs i
cocone_postcompose (cocone_colimit D)
  (Colimit_rec P
     {| legs := legs; legs_comm := legs_comm |}) =
{| legs := legs; legs_comm := legs_comm |}
    srapply path_cocone.H: Funext
G: Graph
D: Diagram G
P: Type
legs: forall i : G, D i -> P
legs_comm: forall (i j : G) (g : G i j),
(fun x : D i => legs j ((D _f g) x)) ==
legs i
forall i : G,
cocone_postcompose (cocone_colimit D)
  (Colimit_rec P
     {| legs := legs; legs_comm := legs_comm |}) i ==
{| legs := legs; legs_comm := legs_comm |} i
H: Funext
G: Graph
D: Diagram G
P: Type
legs: forall i : G, D i -> P
legs_comm: forall (i j : G) (g : G i j),
(fun x : D i => legs j ((D _f g) x)) ==
legs i
forall (i j : G) (g : G i j) 
(x : D i),
Cocone.legs_comm
  (cocone_postcompose (cocone_colimit D)
     (Colimit_rec P
        {| legs := legs; legs_comm := legs_comm |})) i
  j g x @ ?path_legs i x =
?path_legs j ((D _f g) x) @
Cocone.legs_comm
  {| legs := legs; legs_comm := legs_comm |} i j g x
    1: reflexivity.H: Funext
G: Graph
D: Diagram G
P: Type
legs: forall i : G, D i -> P
legs_comm: forall (i j : G) (g : G i j),
(fun x : D i => legs j ((D _f g) x)) ==
legs i
forall (i j : G) (g : G i j) (x : D i),
Cocone.legs_comm
  (cocone_postcompose (cocone_colimit D)
     (Colimit_rec P
        {| legs := legs; legs_comm := legs_comm |})) i
  j g x @ (fun (i0 : G) (x0 : D i0) => 1) i x =
(fun (i0 : G) (x0 : D i0) => 1) j ((D _f g) x) @
Cocone.legs_comm
  {| legs := legs; legs_comm := legs_comm |} i j g x
    intros; cbn.H: Funext
G: Graph
D: Diagram G
P: Type
legs: forall i : G, D i -> P
legs_comm: forall (i j : G) (g : G i j),
(fun x : D i => legs j ((D _f g) x)) ==
legs i
i, j: G
g: G i j
x: D i
ap
  (Colimit_rec P
     {| legs := legs; legs_comm := legs_comm |})
  (colimp i j g x) @ 1 = 1 @ legs_comm i j g x
    apply equiv_p1_1q.H: Funext
G: Graph
D: Diagram G
P: Type
legs: forall i : G, D i -> P
legs_comm: forall (i j : G) (g : G i j),
(fun x : D i => legs j ((D _f g) x)) ==
legs i
i, j: G
g: G i j
x: D i
ap
  (Colimit_rec P
     {| legs := legs; legs_comm := legs_comm |})
  (colimp i j g x) = legs_comm i j g x
    apply Colimit_rec_beta_colimp.
Defined.

Definition equiv_colimit_rec `{Funext} {G : Graph} {D : Diagram G} (P : Type)
  : Cocone D P <~> (Colimit D -> P) := Build_Equiv _ _ _ (isequiv_colimit_rec P).

(** It follows that the HIT Colimit is an abstract colimit. *)
Instance unicocone_colimit `{Funext} {G : Graph} (D : Diagram G)
  : UniversalCocone (cocone_colimit D).H: Funext
G: Graph
D: Diagram G
UniversalCocone (cocone_colimit D)
Proof.H: Funext
G: Graph
D: Diagram G
UniversalCocone (cocone_colimit D)
  srapply Build_UniversalCocone; intro Y.H: Funext
G: Graph
D: Diagram G
Y: Type
IsEquiv (cocone_postcompose (cocone_colimit D))
  (* The goal is to show that [cocone_postcompose (cocone_colimit D)] is an equivalence, but that's the inverse to the equivalence we just defined. *)
  exact (isequiv_inverse (equiv_colimit_rec Y)).
Defined.

Instance iscolimit_colimit `{Funext} {G : Graph} (D : Diagram G)
  : IsColimit D (Colimit D)
  := Build_IsColimit _ (unicocone_colimit D).

(** ** Functoriality of concrete colimits *)

(** We will capitalize [Colimit] in the identifiers to indicate that these definitions relate to the concrete colimit defined above.  Below, we will also get functoriality for abstract colimits, without the capital C.  However, to apply those results to the concrete colimit uses [iscolimit_colimit], which requires [Funext], so it is also useful to give direct proofs of some facts. *)

(** We first work in a more general situation.  Any diagram map [m : D1 => D2] induces a map between the canonical colimit of [D1] and any cocone over [D2].  We use "half" to indicate this situation. *)
Definition functor_Colimit_half {G : Graph} {D1 D2 : Diagram G} (m : DiagramMap D1 D2) {Q} (HQ : Cocone D2 Q)
  : Colimit D1 -> Q.G: Graph
D1, D2: Diagram G
m: DiagramMap D1 D2
Q: Type
HQ: Cocone D2 Q
Colimit D1 -> Q
Proof.G: Graph
D1, D2: Diagram G
m: DiagramMap D1 D2
Q: Type
HQ: Cocone D2 Q
Colimit D1 -> Q
  apply Colimit_rec.G: Graph
D1, D2: Diagram G
m: DiagramMap D1 D2
Q: Type
HQ: Cocone D2 Q
Cocone D1 Q
  exact (cocone_precompose m HQ).
Defined.

Definition functor_Colimit_half_beta_colimp {G : Graph} {D1 D2 : Diagram G} (m : DiagramMap D1 D2) {Q} (HQ : Cocone D2 Q) (i j : G) (g : G i j) (x : D1 i)
  : ap (functor_Colimit_half m HQ) (colimp i j g x) = legs_comm (cocone_precompose m HQ) i j g x
  := Colimit_rec_beta_colimp _ _ _ _ _ _.

(** Homotopic diagram maps induce homotopic maps. *)
Definition functor_Colimit_half_homotopy {G : Graph} {D1 D2 : Diagram G}
  {m1 m2 : DiagramMap D1 D2} (h : DiagramMap_homotopy m1 m2)
  {Q} (HQ : Cocone D2 Q)
  : functor_Colimit_half m1 HQ == functor_Colimit_half m2 HQ.G: Graph
D1, D2: Diagram G
m1, m2: DiagramMap D1 D2
h: DiagramMap_homotopy m1 m2
Q: Type
HQ: Cocone D2 Q
functor_Colimit_half m1 HQ ==
functor_Colimit_half m2 HQ
Proof.G: Graph
D1, D2: Diagram G
m1, m2: DiagramMap D1 D2
h: DiagramMap_homotopy m1 m2
Q: Type
HQ: Cocone D2 Q
functor_Colimit_half m1 HQ ==
functor_Colimit_half m2 HQ
  destruct h as [h_obj h_comm].G: Graph
D1, D2: Diagram G
m1, m2: DiagramMap D1 D2
h_obj: forall i : G, m1 i == m2 i
h_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
DiagramMap_comm m1 g x @
h_obj j ((D1 _f g) x) =
ap (D2 _f g) (h_obj i x) @
DiagramMap_comm m2 g x
Q: Type
HQ: Cocone D2 Q
functor_Colimit_half m1 HQ ==
functor_Colimit_half m2 HQ
  snapply Colimit_rec_homotopy'.G: Graph
D1, D2: Diagram G
m1, m2: DiagramMap D1 D2
h_obj: forall i : G, m1 i == m2 i
h_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
DiagramMap_comm m1 g x @
h_obj j ((D1 _f g) x) =
ap (D2 _f g) (h_obj i x) @
DiagramMap_comm m2 g x
Q: Type
HQ: Cocone D2 Q
forall i : G,
cocone_precompose m1 HQ i == cocone_precompose m2 HQ i
G: Graph
D1, D2: Diagram G
m1, m2: DiagramMap D1 D2
h_obj: forall i : G, m1 i == m2 i
h_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
DiagramMap_comm m1 g x @
h_obj j ((D1 _f g) x) =
ap (D2 _f g) (h_obj i x) @
DiagramMap_comm m2 g x
Q: Type
HQ: Cocone D2 Q
forall (i j : G) (g : G i j) 
(x : D1 i),
legs_comm (cocone_precompose m1 HQ) i j g x @
?h_obj i x =
?h_obj j ((D1 _f g) x) @
legs_comm (cocone_precompose m2 HQ) i j g x
  -G: Graph
D1, D2: Diagram G
m1, m2: DiagramMap D1 D2
h_obj: forall i : G, m1 i == m2 i
h_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
DiagramMap_comm m1 g x @
h_obj j ((D1 _f g) x) =
ap (D2 _f g) (h_obj i x) @
DiagramMap_comm m2 g x
Q: Type
HQ: Cocone D2 Q
forall i : G,
cocone_precompose m1 HQ i == cocone_precompose m2 HQ i intros i x; cbn.G: Graph
D1, D2: Diagram G
m1, m2: DiagramMap D1 D2
h_obj: forall i : G, m1 i == m2 i
h_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
DiagramMap_comm m1 g x @
h_obj j ((D1 _f g) x) =
ap (D2 _f g) (h_obj i x) @
DiagramMap_comm m2 g x
Q: Type
HQ: Cocone D2 Q
i: G
x: D1 i
HQ i (m1 i x) = HQ i (m2 i x) apply ap, h_obj.
  -G: Graph
D1, D2: Diagram G
m1, m2: DiagramMap D1 D2
h_obj: forall i : G, m1 i == m2 i
h_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
DiagramMap_comm m1 g x @
h_obj j ((D1 _f g) x) =
ap (D2 _f g) (h_obj i x) @
DiagramMap_comm m2 g x
Q: Type
HQ: Cocone D2 Q
forall (i j : G) (g : G i j) (x : D1 i),
legs_comm (cocone_precompose m1 HQ) i j g x @
(fun i0 : G =>
 (fun x0 : D1 i0 =>
  ap (HQ i0) (h_obj i0 x0)
  :
  cocone_precompose m1 HQ i0 x0 =
  cocone_precompose m2 HQ i0 x0)
 :
 cocone_precompose m1 HQ i0 ==
 cocone_precompose m2 HQ i0) i x =
(fun i0 : G =>
 (fun x0 : D1 i0 =>
  ap (HQ i0) (h_obj i0 x0)
  :
  cocone_precompose m1 HQ i0 x0 =
  cocone_precompose m2 HQ i0 x0)
 :
 cocone_precompose m1 HQ i0 ==
 cocone_precompose m2 HQ i0) j ((D1 _f g) x) @
legs_comm (cocone_precompose m2 HQ) i j g x intros i j g x; simpl.G: Graph
D1, D2: Diagram G
m1, m2: DiagramMap D1 D2
h_obj: forall i : G, m1 i == m2 i
h_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
DiagramMap_comm m1 g x @
h_obj j ((D1 _f g) x) =
ap (D2 _f g) (h_obj i x) @
DiagramMap_comm m2 g x
Q: Type
HQ: Cocone D2 Q
i, j: G
g: G i j
x: D1 i
(ap (HQ j) (DiagramMap_comm m1 g x)^ @
 legs_comm HQ i j g (m1 i x)) @ ap (HQ i) (h_obj i x) =
ap (HQ j) (h_obj j ((D1 _f g) x)) @
(ap (HQ j) (DiagramMap_comm m2 g x)^ @
 legs_comm HQ i j g (m2 i x))
    Open Scope long_path_scope.G: Graph
D1, D2: Diagram G
m1, m2: DiagramMap D1 D2
h_obj: forall i : G, m1 i == m2 i
h_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
DiagramMap_comm m1 g x
@' h_obj j ((D1 _f g) x) =
ap (D2 _f g) (h_obj i x)
@' DiagramMap_comm m2 g x
Q: Type
HQ: Cocone D2 Q
i, j: G
g: G i j
x: D1 i
ap (HQ j) (DiagramMap_comm m1 g x)^
@' legs_comm HQ i j g (m1 i x)
@' ap (HQ i) (h_obj i x) =
ap (HQ j) (h_obj j ((D1 _f g) x))
@' (ap (HQ j) (DiagramMap_comm m2 g x)^
    @' legs_comm HQ i j g (m2 i x))
    (* TODO: Most of the work here comes from a mismatch between the direction of the path in [DiagramMap_comm] and [legs_comm] in the [Cocone] record, causing a reversal in [cocone_precompose].  There is no reversal in [cocone_postcompose], so I think [Cocone] should change. If that is done, then this result wouldn't be needed at all, and one could directly use [Colimit_rec_homotopy']. *)
    rewrite ap_V.G: Graph
D1, D2: Diagram G
m1, m2: DiagramMap D1 D2
h_obj: forall i : G, m1 i == m2 i
h_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
DiagramMap_comm m1 g x
@' h_obj j ((D1 _f g) x) =
ap (D2 _f g) (h_obj i x)
@' DiagramMap_comm m2 g x
Q: Type
HQ: Cocone D2 Q
i, j: G
g: G i j
x: D1 i
(ap (HQ j) (DiagramMap_comm m1 g x))^
@' legs_comm HQ i j g (m1 i x)
@' ap (HQ i) (h_obj i x) =
ap (HQ j) (h_obj j ((D1 _f g) x))
@' (ap (HQ j) (DiagramMap_comm m2 g x)^
    @' legs_comm HQ i j g (m2 i x))
    lhs napply concat_pp_p.G: Graph
D1, D2: Diagram G
m1, m2: DiagramMap D1 D2
h_obj: forall i : G, m1 i == m2 i
h_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
DiagramMap_comm m1 g x
@' h_obj j ((D1 _f g) x) =
ap (D2 _f g) (h_obj i x)
@' DiagramMap_comm m2 g x
Q: Type
HQ: Cocone D2 Q
i, j: G
g: G i j
x: D1 i
(ap (HQ j) (DiagramMap_comm m1 g x))^
@' (legs_comm HQ i j g (m1 i x)
    @' ap (HQ i) (h_obj i x)) =
ap (HQ j) (h_obj j ((D1 _f g) x))
@' (ap (HQ j) (DiagramMap_comm m2 g x)^
    @' legs_comm HQ i j g (m2 i x))
    apply moveR_Vp.G: Graph
D1, D2: Diagram G
m1, m2: DiagramMap D1 D2
h_obj: forall i : G, m1 i == m2 i
h_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
DiagramMap_comm m1 g x
@' h_obj j ((D1 _f g) x) =
ap (D2 _f g) (h_obj i x)
@' DiagramMap_comm m2 g x
Q: Type
HQ: Cocone D2 Q
i, j: G
g: G i j
x: D1 i
legs_comm HQ i j g (m1 i x)
@' ap (HQ i) (h_obj i x) =
ap (HQ j) (DiagramMap_comm m1 g x)
@' (ap (HQ j) (h_obj j ((D1 _f g) x))
    @' (ap (HQ j) (DiagramMap_comm m2 g x)^
        @' legs_comm HQ i j g (m2 i x)))
    rewrite ! concat_p_pp.G: Graph
D1, D2: Diagram G
m1, m2: DiagramMap D1 D2
h_obj: forall i : G, m1 i == m2 i
h_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
DiagramMap_comm m1 g x
@' h_obj j ((D1 _f g) x) =
ap (D2 _f g) (h_obj i x)
@' DiagramMap_comm m2 g x
Q: Type
HQ: Cocone D2 Q
i, j: G
g: G i j
x: D1 i
legs_comm HQ i j g (m1 i x)
@' ap (HQ i) (h_obj i x) =
ap (HQ j) (DiagramMap_comm m1 g x)
@' ap (HQ j) (h_obj j ((D1 _f g) x))
@' ap (HQ j) (DiagramMap_comm m2 g x)^
@' legs_comm HQ i j g (m2 i x)
    rewrite <- 2 ap_pp.G: Graph
D1, D2: Diagram G
m1, m2: DiagramMap D1 D2
h_obj: forall i : G, m1 i == m2 i
h_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
DiagramMap_comm m1 g x
@' h_obj j ((D1 _f g) x) =
ap (D2 _f g) (h_obj i x)
@' DiagramMap_comm m2 g x
Q: Type
HQ: Cocone D2 Q
i, j: G
g: G i j
x: D1 i
legs_comm HQ i j g (m1 i x)
@' ap (HQ i) (h_obj i x) =
ap (HQ j)
  (DiagramMap_comm m1 g x
   @' h_obj j ((D1 _f g) x)
   @' (DiagramMap_comm m2 g x)^)
@' legs_comm HQ i j g (m2 i x)
    rewrite h_comm.G: Graph
D1, D2: Diagram G
m1, m2: DiagramMap D1 D2
h_obj: forall i : G, m1 i == m2 i
h_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
DiagramMap_comm m1 g x
@' h_obj j ((D1 _f g) x) =
ap (D2 _f g) (h_obj i x)
@' DiagramMap_comm m2 g x
Q: Type
HQ: Cocone D2 Q
i, j: G
g: G i j
x: D1 i
legs_comm HQ i j g (m1 i x)
@' ap (HQ i) (h_obj i x) =
ap (HQ j)
  (ap (D2 _f g) (h_obj i x)
   @' DiagramMap_comm m2 g x
   @' (DiagramMap_comm m2 g x)^)
@' legs_comm HQ i j g (m2 i x)
    rewrite concat_pp_V.G: Graph
D1, D2: Diagram G
m1, m2: DiagramMap D1 D2
h_obj: forall i : G, m1 i == m2 i
h_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
DiagramMap_comm m1 g x
@' h_obj j ((D1 _f g) x) =
ap (D2 _f g) (h_obj i x)
@' DiagramMap_comm m2 g x
Q: Type
HQ: Cocone D2 Q
i, j: G
g: G i j
x: D1 i
legs_comm HQ i j g (m1 i x)
@' ap (HQ i) (h_obj i x) =
ap (HQ j) (ap (D2 _f g) (h_obj i x))
@' legs_comm HQ i j g (m2 i x)
    rewrite <- ap_compose.G: Graph
D1, D2: Diagram G
m1, m2: DiagramMap D1 D2
h_obj: forall i : G, m1 i == m2 i
h_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
DiagramMap_comm m1 g x
@' h_obj j ((D1 _f g) x) =
ap (D2 _f g) (h_obj i x)
@' DiagramMap_comm m2 g x
Q: Type
HQ: Cocone D2 Q
i, j: G
g: G i j
x: D1 i
legs_comm HQ i j g (m1 i x)
@' ap (HQ i) (h_obj i x) =
ap (fun x : D2 i => HQ j ((D2 _f g) x)) (h_obj i x)
@' legs_comm HQ i j g (m2 i x)
    exact (concat_Ap (legs_comm HQ i j g) (h_obj i x))^.
    Close Scope long_path_scope.
Defined.

(** Now we specialize to the case where the second cone is a colimiting cone. *)
Definition functor_Colimit {G : Graph} {D1 D2 : Diagram G} (m : DiagramMap D1 D2)
  : Colimit D1 -> Colimit D2
  := functor_Colimit_half m (cocone_colimit D2).

(** A homotopy between diagram maps [m1, m2 : D1 => D2] gives a homotopy between the induced maps. *)
Definition functor_Colimit_homotopy {G : Graph} {D1 D2 : Diagram G}
  {m1 m2 : DiagramMap D1 D2} (h : DiagramMap_homotopy m1 m2)
  : functor_Colimit m1 == functor_Colimit m2
  := functor_Colimit_half_homotopy h _.

(** Composition of diagram maps commutes with [functor_Colimit_half], provided the first map uses [functor_Colimit]. *)
Definition functor_Colimit_half_compose {G : Graph} {A B C : Diagram G} (f : DiagramMap A B) (g : DiagramMap B C) {Q} (HQ : Cocone C Q)
  : functor_Colimit_half (diagram_comp g f) HQ == functor_Colimit_half g HQ o functor_Colimit f.G: Graph
A, B, C: Diagram G
f: DiagramMap A B
g: DiagramMap B C
Q: Type
HQ: Cocone C Q
functor_Colimit_half (diagram_comp g f) HQ ==
functor_Colimit_half g HQ o functor_Colimit f
Proof.G: Graph
A, B, C: Diagram G
f: DiagramMap A B
g: DiagramMap B C
Q: Type
HQ: Cocone C Q
functor_Colimit_half (diagram_comp g f) HQ ==
functor_Colimit_half g HQ o functor_Colimit f
  snapply Colimit_rec_homotopy.G: Graph
A, B, C: Diagram G
f: DiagramMap A B
g: DiagramMap B C
Q: Type
HQ: Cocone C Q
forall i : G,
cocone_precompose (diagram_comp g f) HQ i ==
(fun x : Colimit A =>
 functor_Colimit_half g HQ (functor_Colimit f x))
o colim i
G: Graph
A, B, C: Diagram G
f: DiagramMap A B
g: DiagramMap B C
Q: Type
HQ: Cocone C Q
forall (i j : G) (g0 : G i j) (x : A i),
legs_comm (cocone_precompose (diagram_comp g f) HQ) i
  j g0 x @ ?h_obj i x =
?h_obj j ((A _f g0) x) @
ap
  (fun x0 : Colimit A =>
   functor_Colimit_half g HQ (functor_Colimit f x0))
  (colimp i j g0 x)
  -G: Graph
A, B, C: Diagram G
f: DiagramMap A B
g: DiagramMap B C
Q: Type
HQ: Cocone C Q
forall i : G,
cocone_precompose (diagram_comp g f) HQ i ==
(fun x : Colimit A =>
 functor_Colimit_half g HQ (functor_Colimit f x))
o colim i reflexivity.
  -G: Graph
A, B, C: Diagram G
f: DiagramMap A B
g: DiagramMap B C
Q: Type
HQ: Cocone C Q
forall (i j : G) (g0 : G i j) (x : A i),
legs_comm (cocone_precompose (diagram_comp g f) HQ) i
  j g0 x @ (fun (i0 : G) (x0 : A i0) => 1) i x =
(fun (i0 : G) (x0 : A i0) => 1) j ((A _f g0) x) @
ap
  (fun x0 : Colimit A =>
   functor_Colimit_half g HQ (functor_Colimit f x0))
  (colimp i j g0 x) intros i j k x; cbn.G: Graph
A, B, C: Diagram G
f: DiagramMap A B
g: DiagramMap B C
Q: Type
HQ: Cocone C Q
i, j: G
k: G i j
x: A i
(ap (HQ j)
   (comm_square_comp (DiagramMap_comm f k)
      (DiagramMap_comm g k) x)^ @
 legs_comm HQ i j k (g i (f i x))) @ 1 =
1 @
ap
  (fun x : Colimit A =>
   functor_Colimit_half g HQ (functor_Colimit f x))
  (colimp i j k x)
    apply equiv_p1_1q.G: Graph
A, B, C: Diagram G
f: DiagramMap A B
g: DiagramMap B C
Q: Type
HQ: Cocone C Q
i, j: G
k: G i j
x: A i
ap (HQ j)
  (comm_square_comp (DiagramMap_comm f k)
     (DiagramMap_comm g k) x)^ @
legs_comm HQ i j k (g i (f i x)) =
ap
  (fun x : Colimit A =>
   functor_Colimit_half g HQ (functor_Colimit f x))
  (colimp i j k x)
    unfold comm_square_comp.G: Graph
A, B, C: Diagram G
f: DiagramMap A B
g: DiagramMap B C
Q: Type
HQ: Cocone C Q
i, j: G
k: G i j
x: A i
ap (HQ j)
  (DiagramMap_comm g k (f i x) @
   ap (g j) (DiagramMap_comm f k x))^ @
legs_comm HQ i j k (g i (f i x)) =
ap
  (fun x : Colimit A =>
   functor_Colimit_half g HQ (functor_Colimit f x))
  (colimp i j k x)
    Open Scope long_path_scope.G: Graph
A, B, C: Diagram G
f: DiagramMap A B
g: DiagramMap B C
Q: Type
HQ: Cocone C Q
i, j: G
k: G i j
x: A i
ap (HQ j)
  (DiagramMap_comm g k (f i x)
   @' ap (g j) (DiagramMap_comm f k x))^
@' legs_comm HQ i j k (g i (f i x)) =
ap
  (fun x : Colimit A =>
   functor_Colimit_half g HQ (functor_Colimit f x))
  (colimp i j k x)
    lhs napply (ap_V _ _ @@ 1).G: Graph
A, B, C: Diagram G
f: DiagramMap A B
g: DiagramMap B C
Q: Type
HQ: Cocone C Q
i, j: G
k: G i j
x: A i
(ap (HQ j)
   (DiagramMap_comm g k (f i x)
    @' ap (g j) (DiagramMap_comm f k x)))^
@' legs_comm HQ i j k (g i (f i x)) =
ap
  (fun x : Colimit A =>
   functor_Colimit_half g HQ (functor_Colimit f x))
  (colimp i j k x)
    lhs napply (inverse2 (ap_pp (HQ j) _ _) @@ 1).G: Graph
A, B, C: Diagram G
f: DiagramMap A B
g: DiagramMap B C
Q: Type
HQ: Cocone C Q
i, j: G
k: G i j
x: A i
(ap (HQ j) (DiagramMap_comm g k (f i x))
 @' ap (HQ j) (ap (g j) (DiagramMap_comm f k x)))^
@' legs_comm HQ i j k (g i (f i x)) =
ap
  (fun x : Colimit A =>
   functor_Colimit_half g HQ (functor_Colimit f x))
  (colimp i j k x)
    lhs napply (inv_pp _ _ @@ 1).G: Graph
A, B, C: Diagram G
f: DiagramMap A B
g: DiagramMap B C
Q: Type
HQ: Cocone C Q
i, j: G
k: G i j
x: A i
(ap (HQ j) (ap (g j) (DiagramMap_comm f k x)))^
@' (ap (HQ j) (DiagramMap_comm g k (f i x)))^
@' legs_comm HQ i j k (g i (f i x)) =
ap
  (fun x : Colimit A =>
   functor_Colimit_half g HQ (functor_Colimit f x))
  (colimp i j k x)
    symmetry.G: Graph
A, B, C: Diagram G
f: DiagramMap A B
g: DiagramMap B C
Q: Type
HQ: Cocone C Q
i, j: G
k: G i j
x: A i
ap
  (fun x : Colimit A =>
   functor_Colimit_half g HQ (functor_Colimit f x))
  (colimp i j k x) =
(ap (HQ j) (ap (g j) (DiagramMap_comm f k x)))^
@' (ap (HQ j) (DiagramMap_comm g k (f i x)))^
@' legs_comm HQ i j k (g i (f i x))
    lhs napply (ap_compose (functor_Colimit f)).G: Graph
A, B, C: Diagram G
f: DiagramMap A B
g: DiagramMap B C
Q: Type
HQ: Cocone C Q
i, j: G
k: G i j
x: A i
ap (functor_Colimit_half g HQ)
  (ap (functor_Colimit f) (colimp i j k x)) =
(ap (HQ j) (ap (g j) (DiagramMap_comm f k x)))^
@' (ap (HQ j) (DiagramMap_comm g k (f i x)))^
@' legs_comm HQ i j k (g i (f i x))
    lhs napply (ap _ (Colimit_rec_beta_colimp _ _ _ _ _ _)).G: Graph
A, B, C: Diagram G
f: DiagramMap A B
g: DiagramMap B C
Q: Type
HQ: Cocone C Q
i, j: G
k: G i j
x: A i
ap (functor_Colimit_half g HQ)
  (legs_comm (cocone_precompose f (cocone_colimit B))
     i j k x) =
(ap (HQ j) (ap (g j) (DiagramMap_comm f k x)))^
@' (ap (HQ j) (DiagramMap_comm g k (f i x)))^
@' legs_comm HQ i j k (g i (f i x))
    (* [legs_comm] unfolds to a composite of paths, but the next line works best without unfolding it. *)
    lhs napply ap_pp.G: Graph
A, B, C: Diagram G
f: DiagramMap A B
g: DiagramMap B C
Q: Type
HQ: Cocone C Q
i, j: G
k: G i j
x: A i
ap (functor_Colimit_half g HQ)
  (ap (cocone_colimit B j) (DiagramMap_comm f k x)^)
@' ap (functor_Colimit_half g HQ)
     (legs_comm (cocone_colimit B) i j k (f i x)) =
(ap (HQ j) (ap (g j) (DiagramMap_comm f k x)))^
@' (ap (HQ j) (DiagramMap_comm g k (f i x)))^
@' legs_comm HQ i j k (g i (f i x))
    lhs nrefine (1 @@ _).G: Graph
A, B, C: Diagram G
f: DiagramMap A B
g: DiagramMap B C
Q: Type
HQ: Cocone C Q
i, j: G
k: G i j
x: A i
ap (functor_Colimit_half g HQ)
  (legs_comm (cocone_colimit B) i j k (f i x)) = ?Goal
G: Graph
A, B, C: Diagram G
f: DiagramMap A B
g: DiagramMap B C
Q: Type
HQ: Cocone C Q
i, j: G
k: G i j
x: A i
ap (functor_Colimit_half g HQ)
  (ap (cocone_colimit B j) (DiagramMap_comm f k x)^)
@' ?Goal =
(ap (HQ j) (ap (g j) (DiagramMap_comm f k x)))^
@' (ap (HQ j) (DiagramMap_comm g k (f i x)))^
@' legs_comm HQ i j k (g i (f i x)) 1: napply functor_Colimit_half_beta_colimp.G: Graph
A, B, C: Diagram G
f: DiagramMap A B
g: DiagramMap B C
Q: Type
HQ: Cocone C Q
i, j: G
k: G i j
x: A i
ap (functor_Colimit_half g HQ)
  (ap (cocone_colimit B j) (DiagramMap_comm f k x)^)
@' legs_comm (cocone_precompose g HQ) i j k (f i x) =
(ap (HQ j) (ap (g j) (DiagramMap_comm f k x)))^
@' (ap (HQ j) (DiagramMap_comm g k (f i x)))^
@' legs_comm HQ i j k (g i (f i x))
    simpl.G: Graph
A, B, C: Diagram G
f: DiagramMap A B
g: DiagramMap B C
Q: Type
HQ: Cocone C Q
i, j: G
k: G i j
x: A i
ap (functor_Colimit_half g HQ)
  (ap (colim j) (DiagramMap_comm f k x)^)
@' (ap (HQ j) (DiagramMap_comm g k (f i x))^
    @' legs_comm HQ i j k (g i (f i x))) =
(ap (HQ j) (ap (g j) (DiagramMap_comm f k x)))^
@' (ap (HQ j) (DiagramMap_comm g k (f i x)))^
@' legs_comm HQ i j k (g i (f i x))
    lhs napply concat_p_pp.G: Graph
A, B, C: Diagram G
f: DiagramMap A B
g: DiagramMap B C
Q: Type
HQ: Cocone C Q
i, j: G
k: G i j
x: A i
ap (functor_Colimit_half g HQ)
  (ap (colim j) (DiagramMap_comm f k x)^)
@' ap (HQ j) (DiagramMap_comm g k (f i x))^
@' legs_comm HQ i j k (g i (f i x)) =
(ap (HQ j) (ap (g j) (DiagramMap_comm f k x)))^
@' (ap (HQ j) (DiagramMap_comm g k (f i x)))^
@' legs_comm HQ i j k (g i (f i x))
    nrefine (_ @@ 1).G: Graph
A, B, C: Diagram G
f: DiagramMap A B
g: DiagramMap B C
Q: Type
HQ: Cocone C Q
i, j: G
k: G i j
x: A i
ap (functor_Colimit_half g HQ)
  (ap (colim j) (DiagramMap_comm f k x)^)
@' ap (HQ j) (DiagramMap_comm g k (f i x))^ =
(ap (HQ j) (ap (g j) (DiagramMap_comm f k x)))^
@' (ap (HQ j) (DiagramMap_comm g k (f i x)))^
    apply ap011.G: Graph
A, B, C: Diagram G
f: DiagramMap A B
g: DiagramMap B C
Q: Type
HQ: Cocone C Q
i, j: G
k: G i j
x: A i
ap (functor_Colimit_half g HQ)
  (ap (colim j) (DiagramMap_comm f k x)^) =
(ap (HQ j) (ap (g j) (DiagramMap_comm f k x)))^
G: Graph
A, B, C: Diagram G
f: DiagramMap A B
g: DiagramMap B C
Q: Type
HQ: Cocone C Q
i, j: G
k: G i j
x: A i
ap (HQ j) (DiagramMap_comm g k (f i x))^ =
(ap (HQ j) (DiagramMap_comm g k (f i x)))^
    2: napply ap_V.G: Graph
A, B, C: Diagram G
f: DiagramMap A B
g: DiagramMap B C
Q: Type
HQ: Cocone C Q
i, j: G
k: G i j
x: A i
ap (functor_Colimit_half g HQ)
  (ap (colim j) (DiagramMap_comm f k x)^) =
(ap (HQ j) (ap (g j) (DiagramMap_comm f k x)))^
    lhs_V napply (ap_compose (colim j)); simpl.G: Graph
A, B, C: Diagram G
f: DiagramMap A B
g: DiagramMap B C
Q: Type
HQ: Cocone C Q
i, j: G
k: G i j
x: A i
ap (fun x : B j => HQ j (g j x))
  (DiagramMap_comm f k x)^ =
(ap (HQ j) (ap (g j) (DiagramMap_comm f k x)))^
    lhs napply (ap_V (HQ j o g j) _).G: Graph
A, B, C: Diagram G
f: DiagramMap A B
g: DiagramMap B C
Q: Type
HQ: Cocone C Q
i, j: G
k: G i j
x: A i
(ap (fun x : B j => HQ j (g j x))
   (DiagramMap_comm f k x))^ =
(ap (HQ j) (ap (g j) (DiagramMap_comm f k x)))^
    apply ap, ap_compose.
    Close Scope long_path_scope.
Defined.

(** ** Functoriality of abstract colimits *)

Section FunctorialityColimit.

  Context `{Funext} {G : Graph}.

  (** Colimits are preserved by composition with a (diagram) equivalence. *)

  Definition iscolimit_precompose_equiv {D1 D2 : Diagram G}
    (m : D1 ~d~ D2) {Q : Type}
    : IsColimit D2 Q -> IsColimit D1 Q.H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q: Type
IsColimit D2 Q -> IsColimit D1 Q
  Proof.H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q: Type
IsColimit D2 Q -> IsColimit D1 Q
    intros HQ.H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q: Type
HQ: IsColimit D2 Q
IsColimit D1 Q
    srapply (Build_IsColimit (cocone_precompose m HQ) _).H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q: Type
HQ: IsColimit D2 Q
UniversalCocone (cocone_precompose m HQ)
    apply cocone_precompose_equiv_universality, HQ.
  Defined.

  Definition iscolimit_postcompose_equiv {D: Diagram G} `(f: Q <~> Q')
    : IsColimit D Q -> IsColimit D Q'.H: Funext
G: Graph
D: Diagram G
Q, Q': Type
f: Q <~> Q'
IsColimit D Q -> IsColimit D Q'
  Proof.H: Funext
G: Graph
D: Diagram G
Q, Q': Type
f: Q <~> Q'
IsColimit D Q -> IsColimit D Q'
    intros HQ.H: Funext
G: Graph
D: Diagram G
Q, Q': Type
f: Q <~> Q'
HQ: IsColimit D Q
IsColimit D Q'
    srapply (Build_IsColimit (cocone_postcompose HQ f) _).H: Funext
G: Graph
D: Diagram G
Q, Q': Type
f: Q <~> Q'
HQ: IsColimit D Q
UniversalCocone (cocone_postcompose HQ f)
    apply cocone_postcompose_equiv_universality, HQ.
  Defined.

  (** A diagram map [m : D1 => D2] induces a map between any two colimits of [D1] and [D2]. *)
  Definition functor_colimit {D1 D2 : Diagram G} (m : DiagramMap D1 D2)
    {Q1 Q2} (HQ1 : IsColimit D1 Q1) (HQ2 : IsColimit D2 Q2)
    : Q1 -> Q2 := cocone_postcompose_inv HQ1 (cocone_precompose m HQ2).

  (** And this map commutes with diagram map. *)
  Definition functor_colimit_commute {D1 D2 : Diagram G}
    (m : DiagramMap D1 D2) {Q1 Q2}
    (HQ1 : IsColimit D1 Q1) (HQ2: IsColimit D2 Q2)
    : cocone_precompose m HQ2
      = cocone_postcompose HQ1 (functor_colimit m HQ1 HQ2)
    := (eisretr (cocone_postcompose HQ1) _)^.

  (** Additional coherence with postcompose and precompose. *)
  Definition cocone_precompose_postcompose_comp {D1 D2 : Diagram G}
    (m : DiagramMap D1 D2) {Q1 Q2 : Type} (HQ1 : IsColimit D1 Q1)
    (HQ2 : IsColimit D2 Q2) {T : Type} (t : Q2 -> T)
    : cocone_postcompose HQ1 (t o functor_colimit m HQ1 HQ2)
      = cocone_precompose m (cocone_postcompose HQ2 t).H: Funext
G: Graph
D1, D2: Diagram G
m: DiagramMap D1 D2
Q1, Q2: Type
HQ1: IsColimit D1 Q1
HQ2: IsColimit D2 Q2
T: Type
t: Q2 -> T
cocone_postcompose HQ1 (t o functor_colimit m HQ1 HQ2) =
cocone_precompose m (cocone_postcompose HQ2 t)
    Proof.H: Funext
G: Graph
D1, D2: Diagram G
m: DiagramMap D1 D2
Q1, Q2: Type
HQ1: IsColimit D1 Q1
HQ2: IsColimit D2 Q2
T: Type
t: Q2 -> T
cocone_postcompose HQ1 (t o functor_colimit m HQ1 HQ2) =
cocone_precompose m (cocone_postcompose HQ2 t)
      lhs napply cocone_postcompose_comp.H: Funext
G: Graph
D1, D2: Diagram G
m: DiagramMap D1 D2
Q1, Q2: Type
HQ1: IsColimit D1 Q1
HQ2: IsColimit D2 Q2
T: Type
t: Q2 -> T
cocone_postcompose
  (cocone_postcompose HQ1 (functor_colimit m HQ1 HQ2))
  t = cocone_precompose m (cocone_postcompose HQ2 t)
      lhs_V exact (ap (fun x => cocone_postcompose x t)
        (functor_colimit_commute m HQ1 HQ2)).H: Funext
G: Graph
D1, D2: Diagram G
m: DiagramMap D1 D2
Q1, Q2: Type
HQ1: IsColimit D1 Q1
HQ2: IsColimit D2 Q2
T: Type
t: Q2 -> T
cocone_postcompose (cocone_precompose m HQ2) t =
cocone_precompose m (cocone_postcompose HQ2 t)
      napply cocone_precompose_postcompose.
    Defined.

  (** In order to show that colimits are functorial, we show that this is true after precomposing with the cocone. *)
  Definition postcompose_functor_colimit_compose {D1 D2 D3 : Diagram G}
    (m : DiagramMap D1 D2) (n : DiagramMap D2 D3)
    {Q1 Q2 Q3} (HQ1 : IsColimit D1 Q1) (HQ2 : IsColimit D2 Q2)
    (HQ3 : IsColimit D3 Q3)
    : cocone_postcompose HQ1 (functor_colimit n HQ2 HQ3 o functor_colimit m HQ1 HQ2)
      = cocone_postcompose HQ1 (functor_colimit (diagram_comp n m) HQ1 HQ3).H: Funext
G: Graph
D1, D2, D3: Diagram G
m: DiagramMap D1 D2
n: DiagramMap D2 D3
Q1, Q2, Q3: Type
HQ1: IsColimit D1 Q1
HQ2: IsColimit D2 Q2
HQ3: IsColimit D3 Q3
cocone_postcompose HQ1
  (functor_colimit n HQ2 HQ3
   o functor_colimit m HQ1 HQ2) =
cocone_postcompose HQ1
  (functor_colimit (diagram_comp n m) HQ1 HQ3)
  Proof.H: Funext
G: Graph
D1, D2, D3: Diagram G
m: DiagramMap D1 D2
n: DiagramMap D2 D3
Q1, Q2, Q3: Type
HQ1: IsColimit D1 Q1
HQ2: IsColimit D2 Q2
HQ3: IsColimit D3 Q3
cocone_postcompose HQ1
  (functor_colimit n HQ2 HQ3
   o functor_colimit m HQ1 HQ2) =
cocone_postcompose HQ1
  (functor_colimit (diagram_comp n m) HQ1 HQ3)
    lhs napply cocone_precompose_postcompose_comp.H: Funext
G: Graph
D1, D2, D3: Diagram G
m: DiagramMap D1 D2
n: DiagramMap D2 D3
Q1, Q2, Q3: Type
HQ1: IsColimit D1 Q1
HQ2: IsColimit D2 Q2
HQ3: IsColimit D3 Q3
cocone_precompose m
  (cocone_postcompose HQ2 (functor_colimit n HQ2 HQ3)) =
cocone_postcompose HQ1
  (functor_colimit (diagram_comp n m) HQ1 HQ3)
    lhs_V napply (ap _ (functor_colimit_commute n HQ2 HQ3)).H: Funext
G: Graph
D1, D2, D3: Diagram G
m: DiagramMap D1 D2
n: DiagramMap D2 D3
Q1, Q2, Q3: Type
HQ1: IsColimit D1 Q1
HQ2: IsColimit D2 Q2
HQ3: IsColimit D3 Q3
cocone_precompose m (cocone_precompose n HQ3) =
cocone_postcompose HQ1
  (functor_colimit (diagram_comp n m) HQ1 HQ3)
    lhs napply cocone_precompose_comp.H: Funext
G: Graph
D1, D2, D3: Diagram G
m: DiagramMap D1 D2
n: DiagramMap D2 D3
Q1, Q2, Q3: Type
HQ1: IsColimit D1 Q1
HQ2: IsColimit D2 Q2
HQ3: IsColimit D3 Q3
cocone_precompose (diagram_comp n m) HQ3 =
cocone_postcompose HQ1
  (functor_colimit (diagram_comp n m) HQ1 HQ3)
    napply functor_colimit_commute.
  Defined.

  Definition functor_colimit_compose {D1 D2 D3 : Diagram G}
    (m : DiagramMap D1 D2) (n : DiagramMap D2 D3)
    {Q1 Q2 Q3} (HQ1 : IsColimit D1 Q1) (HQ2 : IsColimit D2 Q2)
    (HQ3 : IsColimit D3 Q3)
    : functor_colimit n HQ2 HQ3 o functor_colimit m HQ1 HQ2
      = functor_colimit (diagram_comp n m) HQ1 HQ3
    := @equiv_inj _ _
      (cocone_postcompose HQ1) (iscolimit_unicocone HQ1 Q3) _ _
      (postcompose_functor_colimit_compose m n HQ1 HQ2 HQ3).

  (** ** Colimits of equivalent diagrams *)

  (** Now we have that two equivalent diagrams have equivalent colimits. *)

  Context {D1 D2 : Diagram G} (m : D1 ~d~ D2) {Q1 Q2}
    (HQ1 : IsColimit D1 Q1) (HQ2 : IsColimit D2 Q2).

  Definition functor_colimit_eissect
    : functor_colimit m HQ1 HQ2
      o functor_colimit (diagram_equiv_inv m) HQ2 HQ1 == idmap.H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsColimit D1 Q1
HQ2: IsColimit D2 Q2
functor_colimit m HQ1 HQ2
o functor_colimit (diagram_equiv_inv m) HQ2 HQ1 ==
idmap
  Proof.H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsColimit D1 Q1
HQ2: IsColimit D2 Q2
functor_colimit m HQ1 HQ2
o functor_colimit (diagram_equiv_inv m) HQ2 HQ1 ==
idmap
    apply ap10.H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsColimit D1 Q1
HQ2: IsColimit D2 Q2
(fun x : Q2 =>
 functor_colimit m HQ1 HQ2
   (functor_colimit (diagram_equiv_inv m) HQ2 HQ1 x)) =
idmap
    srapply (equiv_inj (cocone_postcompose HQ2) _).H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsColimit D1 Q1
HQ2: IsColimit D2 Q2
IsEquiv (cocone_postcompose HQ2)
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsColimit D1 Q1
HQ2: IsColimit D2 Q2
cocone_postcompose HQ2
  (fun x : Q2 =>
   functor_colimit m HQ1 HQ2
     (functor_colimit (diagram_equiv_inv m) HQ2 HQ1 x)) =
cocone_postcompose HQ2 idmap
    1: apply HQ2.H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsColimit D1 Q1
HQ2: IsColimit D2 Q2
cocone_postcompose HQ2
  (fun x : Q2 =>
   functor_colimit m HQ1 HQ2
     (functor_colimit (diagram_equiv_inv m) HQ2 HQ1 x)) =
cocone_postcompose HQ2 idmap
    etransitivity.H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsColimit D1 Q1
HQ2: IsColimit D2 Q2
cocone_postcompose HQ2
  (fun x : Q2 =>
   functor_colimit m HQ1 HQ2
     (functor_colimit (diagram_equiv_inv m) HQ2 HQ1 x)) =
?Goal
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsColimit D1 Q1
HQ2: IsColimit D2 Q2
?Goal = cocone_postcompose HQ2 idmap
    2:symmetry; apply cocone_postcompose_identity.H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsColimit D1 Q1
HQ2: IsColimit D2 Q2
cocone_postcompose HQ2
  (fun x : Q2 =>
   functor_colimit m HQ1 HQ2
     (functor_colimit (diagram_equiv_inv m) HQ2 HQ1 x)) =
HQ2
    etransitivity.H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsColimit D1 Q1
HQ2: IsColimit D2 Q2
cocone_postcompose HQ2
  (fun x : Q2 =>
   functor_colimit m HQ1 HQ2
     (functor_colimit (diagram_equiv_inv m) HQ2 HQ1 x)) =
?Goal
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsColimit D1 Q1
HQ2: IsColimit D2 Q2
?Goal = HQ2
    1: apply cocone_postcompose_comp.H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsColimit D1 Q1
HQ2: IsColimit D2 Q2
cocone_postcompose
  (cocone_postcompose HQ2
     (functor_colimit (diagram_equiv_inv m) HQ2 HQ1))
  (functor_colimit m HQ1 HQ2) = HQ2
    rewrite eisretr, cocone_precompose_postcompose, eisretr.H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsColimit D1 Q1
HQ2: IsColimit D2 Q2
cocone_precompose (diagram_equiv_inv m)
  (cocone_precompose m HQ2) = HQ2
    rewrite cocone_precompose_comp, diagram_inv_is_section.H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsColimit D1 Q1
HQ2: IsColimit D2 Q2
cocone_precompose (diagram_idmap D2) HQ2 = HQ2
    apply cocone_precompose_identity.
  Defined.

  Definition functor_colimit_eisretr
    : functor_colimit (diagram_equiv_inv m) HQ2 HQ1
      o functor_colimit m HQ1 HQ2 == idmap.H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsColimit D1 Q1
HQ2: IsColimit D2 Q2
functor_colimit (diagram_equiv_inv m) HQ2 HQ1
o functor_colimit m HQ1 HQ2 == idmap
  Proof.H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsColimit D1 Q1
HQ2: IsColimit D2 Q2
functor_colimit (diagram_equiv_inv m) HQ2 HQ1
o functor_colimit m HQ1 HQ2 == idmap
    apply ap10.H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsColimit D1 Q1
HQ2: IsColimit D2 Q2
(fun x : Q1 =>
 functor_colimit (diagram_equiv_inv m) HQ2 HQ1
   (functor_colimit m HQ1 HQ2 x)) = idmap
    srapply (equiv_inj (cocone_postcompose HQ1) _).H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsColimit D1 Q1
HQ2: IsColimit D2 Q2
IsEquiv (cocone_postcompose HQ1)
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsColimit D1 Q1
HQ2: IsColimit D2 Q2
cocone_postcompose HQ1
  (fun x : Q1 =>
   functor_colimit (diagram_equiv_inv m) HQ2 HQ1
     (functor_colimit m HQ1 HQ2 x)) =
cocone_postcompose HQ1 idmap
    1: apply HQ1.H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsColimit D1 Q1
HQ2: IsColimit D2 Q2
cocone_postcompose HQ1
  (fun x : Q1 =>
   functor_colimit (diagram_equiv_inv m) HQ2 HQ1
     (functor_colimit m HQ1 HQ2 x)) =
cocone_postcompose HQ1 idmap
    etransitivity.H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsColimit D1 Q1
HQ2: IsColimit D2 Q2
cocone_postcompose HQ1
  (fun x : Q1 =>
   functor_colimit (diagram_equiv_inv m) HQ2 HQ1
     (functor_colimit m HQ1 HQ2 x)) = ?Goal
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsColimit D1 Q1
HQ2: IsColimit D2 Q2
?Goal = cocone_postcompose HQ1 idmap
    2:symmetry; apply cocone_postcompose_identity.H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsColimit D1 Q1
HQ2: IsColimit D2 Q2
cocone_postcompose HQ1
  (fun x : Q1 =>
   functor_colimit (diagram_equiv_inv m) HQ2 HQ1
     (functor_colimit m HQ1 HQ2 x)) = HQ1
    etransitivity.H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsColimit D1 Q1
HQ2: IsColimit D2 Q2
cocone_postcompose HQ1
  (fun x : Q1 =>
   functor_colimit (diagram_equiv_inv m) HQ2 HQ1
     (functor_colimit m HQ1 HQ2 x)) = ?Goal
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsColimit D1 Q1
HQ2: IsColimit D2 Q2
?Goal = HQ1
    1: apply cocone_postcompose_comp.H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsColimit D1 Q1
HQ2: IsColimit D2 Q2
cocone_postcompose
  (cocone_postcompose HQ1 (functor_colimit m HQ1 HQ2))
  (functor_colimit (diagram_equiv_inv m) HQ2 HQ1) =
HQ1
    rewrite eisretr, cocone_precompose_postcompose, eisretr.H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsColimit D1 Q1
HQ2: IsColimit D2 Q2
cocone_precompose m
  (cocone_precompose (diagram_equiv_inv m) HQ1) = HQ1
    rewrite cocone_precompose_comp, diagram_inv_is_retraction.H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsColimit D1 Q1
HQ2: IsColimit D2 Q2
cocone_precompose (diagram_idmap D1) HQ1 = HQ1
    apply cocone_precompose_identity.
  Defined.

  #[export] Instance isequiv_functor_colimit
    : IsEquiv (functor_colimit m HQ1 HQ2)
    := isequiv_adjointify _ _
      functor_colimit_eissect functor_colimit_eisretr.

  Definition equiv_functor_colimit : Q1 <~> Q2
    := Build_Equiv _ _ _ isequiv_functor_colimit.

End FunctorialityColimit.

(** ** Unicity of colimits *)

(** A particular case of the functoriality result is that all colimits of a diagram are equivalent (and hence equal in presence of univalence). *)
Theorem colimit_unicity `{Funext} {G : Graph} {D : Diagram G} {Q1 Q2 : Type}
  (HQ1 : IsColimit D Q1) (HQ2 : IsColimit D Q2)
  : Q1 <~> Q2.H: Funext
G: Graph
D: Diagram G
Q1, Q2: Type
HQ1: IsColimit D Q1
HQ2: IsColimit D Q2
Q1 <~> Q2
Proof.H: Funext
G: Graph
D: Diagram G
Q1, Q2: Type
HQ1: IsColimit D Q1
HQ2: IsColimit D Q2
Q1 <~> Q2
  srapply equiv_functor_colimit.H: Funext
G: Graph
D: Diagram G
Q1, Q2: Type
HQ1: IsColimit D Q1
HQ2: IsColimit D Q2
D ~d~ D
  srapply (Build_diagram_equiv (diagram_idmap D)).
Defined.

(** ** Colimits are left adjoint to constant diagram *)

Theorem colimit_adjoint `{Funext} {G : Graph} {D : Diagram G} {C : Type}
  : (Colimit D -> C) <~> DiagramMap D (diagram_const C).H: Funext
G: Graph
D: Diagram G
C: Type
(Colimit D -> C) <~> DiagramMap D (diagram_const C)
Proof.H: Funext
G: Graph
D: Diagram G
C: Type
(Colimit D -> C) <~> DiagramMap D (diagram_const C)
  symmetry.H: Funext
G: Graph
D: Diagram G
C: Type
DiagramMap D (diagram_const C) <~> (Colimit D -> C)
  refine (equiv_colimit_rec C oE _).H: Funext
G: Graph
D: Diagram G
C: Type
DiagramMap D (diagram_const C) <~> Cocone D C
  apply equiv_diagram_const_cocone.
Defined.