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 Colimits.Coeq.

Local Open Scope path_scope.
Generalizable All Variables.

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

(** * Colimits *)

(** 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;
}.
(* Use :> and remove the two following lines,
   once Coq 8.16 is the minimum required version. *)
#[export] Existing Instance 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 *)

(** Whatever the diagram considered, there exists a colimit of it. The existence is given by the HIT [colimit]. *)

(** ** Definition of the 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
  .
>>
*)

(** A colimit is just 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))^.

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
  srapply (Colimit_ind_beta_colimp (fun _ => P) C _ i j g x).
Defined.

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

(** Colimit_rec is an equivalence *)

Global 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 intro f.H: Funext
G: Graph
D: Diagram G
P: Type
f: Colimit D -> P
Cocone D P
    srapply Build_Cocone.H: Funext
G: Graph
D: Diagram G
P: Type
f: Colimit D -> P
forall i : G, D i -> P
H: Funext
G: Graph
D: Diagram G
P: Type
f: Colimit D -> P
forall (i j : G) (g : G i j),
?legs j o D _f g == ?legs i
    1: intros i g; apply f, (colim i g).H: Funext
G: Graph
D: Diagram G
P: Type
f: Colimit D -> P
forall (i j : G) (g : G i j),
(fun (i0 : G) (g0 : D i0) => f (colim i0 g0)) j
o D _f g ==
(fun (i0 : G) (g0 : D i0) => f (colim i0 g0)) i
    intros i j g x.H: Funext
G: Graph
D: Diagram G
P: Type
f: Colimit D -> P
i, j: G
g: G i j
x: D i
f (colim j ((D _f g) x)) = f (colim i x)
    apply ap, colimp. }H: Funext
G: Graph
D: Diagram G
P: Type
Colimit_rec P
o (fun f : Colimit D -> P =>
   {|
     legs := fun (i : G) (g : D i) => f (colim i g);
     legs_comm :=
       fun (i j : G) (g : G i j) =>
       (fun x : D i => ap f (colimp i j g x))
       :
       (fun (i0 : G) (g0 : D i0) => f (colim i0 g0)) j
       o D _f g ==
       (fun (i0 : G) (g0 : D i0) => f (colim i0 g0)) i
   |}) == idmap
H: Funext
G: Graph
D: Diagram G
P: Type
(fun f : Colimit D -> P =>
 {|
   legs := fun (i : G) (g : D i) => f (colim i g);
   legs_comm :=
     fun (i j : G) (g : G i j) =>
     (fun x : D i => ap f (colimp i j g x))
     :
     (fun (i0 : G) (g0 : D i0) => f (colim i0 g0)) j
     o D _f g ==
     (fun (i0 : G) (g0 : D i0) => f (colim i0 g0)) i
 |}) o Colimit_rec P == idmap
  {H: Funext
G: Graph
D: Diagram G
P: Type
Colimit_rec P
o (fun f : Colimit D -> P =>
   {|
     legs := fun (i : G) (g : D i) => f (colim i g);
     legs_comm :=
       fun (i j : G) (g : G i j) =>
       (fun x : D i => ap f (colimp i j g x))
       :
       (fun (i0 : G) (g0 : D i0) => f (colim i0 g0)) j
       o D _f g ==
       (fun (i0 : G) (g0 : D i0) => f (colim i0 g0)) i
   |}) == idmap intro.H: Funext
G: Graph
D: Diagram G
P: Type
x: Colimit D -> P
Colimit_rec P
  {|
    legs := fun (i : G) (g : D i) => x (colim i g);
    legs_comm :=
      fun (i j : G) (g : G i j) (x0 : D i) =>
      ap x (colimp i j g x0)
  |} = x
    apply path_forall.H: Funext
G: Graph
D: Diagram G
P: Type
x: Colimit D -> P
Colimit_rec P
  {|
    legs := fun (i : G) (g : D i) => x (colim i g);
    legs_comm :=
      fun (i j : G) (g : G i j) (x0 : D i) =>
      ap x (colimp i j g x0)
  |} == x
    srapply Colimit_ind.H: Funext
G: Graph
D: Diagram G
P: Type
x: Colimit D -> P
forall (i : G) (x0 : D i),
(fun w : Colimit D =>
 Colimit_rec P
   {|
     legs := fun (i0 : G) (g : D i0) => x (colim i0 g);
     legs_comm :=
       fun (i0 j : G) (g : G i0 j) (x1 : D i0) =>
       ap x (colimp i0 j g x1)
   |} w = x w) (colim i x0)
H: Funext
G: Graph
D: Diagram G
P: Type
x: Colimit D -> P
forall (i j : G) (g : G i j) (x0 : D i),
transport
  (fun w : Colimit D =>
   Colimit_rec P
     {|
       legs :=
         fun (i0 : G) (g0 : D i0) => x (colim i0 g0);
       legs_comm :=
         fun (i0 j0 : G) (g0 : G i0 j0) (x1 : D i0) =>
         ap x (colimp i0 j0 g0 x1)
     |} w = x w) (colimp i j g x0)
  (?q j ((D _f g) x0)) = ?q i x0
    1: reflexivity.H: Funext
G: Graph
D: Diagram G
P: Type
x: Colimit D -> P
forall (i j : G) (g : G i j) (x0 : D i),
transport
  (fun w : Colimit D =>
   Colimit_rec P
     {|
       legs :=
         fun (i0 : G) (g0 : D i0) => x (colim i0 g0);
       legs_comm :=
         fun (i0 j0 : G) (g0 : G i0 j0) (x1 : D i0) =>
         ap x (colimp i0 j0 g0 x1)
     |} w = x w) (colimp i j g x0)
  ((fun (i0 : G) (x1 : D i0) => 1) j ((D _f g) x0)) =
(fun (i0 : G) (x1 : D i0) => 1) i x0
    intros ????; cbn.H: Funext
G: Graph
D: Diagram G
P: Type
x: Colimit D -> P
i, j: G
g: G i j
x0: D i
transport
  (fun w : Colimit D =>
   Colimit_rec P
     {|
       legs := fun (i : G) (g : D i) => x (colim i g);
       legs_comm :=
         fun (i j : G) (g : G i j) (x0 : D i) =>
         ap x (colimp i j g x0)
     |} w = x w) (colimp i j g x0) 1 = 1
    nrapply transport_paths_FlFr'.H: Funext
G: Graph
D: Diagram G
P: Type
x: Colimit D -> P
i, j: G
g: G i j
x0: D i
ap
  (Colimit_rec P
     {|
       legs := fun (i : G) (g : D i) => x (colim i g);
       legs_comm :=
         fun (i j : G) (g : G i j) (x0 : D i) =>
         ap x (colimp i j g x0)
     |}) (colimp i j g x0) @ 1 =
1 @ ap x (colimp i j g x0)
    apply equiv_p1_1q.H: Funext
G: Graph
D: Diagram G
P: Type
x: Colimit D -> P
i, j: G
g: G i j
x0: D i
ap
  (Colimit_rec P
     {|
       legs := fun (i : G) (g : D i) => x (colim i g);
       legs_comm :=
         fun (i j : G) (g : G i j) (x0 : D i) =>
         ap x (colimp i j g x0)
     |}) (colimp i j g x0) = ap x (colimp i j g x0)
    apply Colimit_rec_beta_colimp. }H: Funext
G: Graph
D: Diagram G
P: Type
(fun f : Colimit D -> P =>
 {|
   legs := fun (i : G) (g : D i) => f (colim i g);
   legs_comm :=
     fun (i j : G) (g : G i j) =>
     (fun x : D i => ap f (colimp i j g x))
     :
     (fun (i0 : G) (g0 : D i0) => f (colim i0 g0)) j
     o D _f g ==
     (fun (i0 : G) (g0 : D i0) => f (colim i0 g0)) i
 |}) o Colimit_rec P == idmap
  {H: Funext
G: Graph
D: Diagram G
P: Type
(fun f : Colimit D -> P =>
 {|
   legs := fun (i : G) (g : D i) => f (colim i g);
   legs_comm :=
     fun (i j : G) (g : G i j) =>
     (fun x : D i => ap f (colimp i j g x))
     :
     (fun (i0 : G) (g0 : D i0) => f (colim i0 g0)) j
     o D _f g ==
     (fun (i0 : G) (g0 : D i0) => f (colim i0 g0)) i
 |}) 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
{|
  legs :=
    fun (i : G) (g : D i) =>
    Colimit_rec P
      {| legs := legs; legs_comm := legs_comm |}
      (colim i g);
  legs_comm :=
    fun (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 := 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,
{|
  legs :=
    fun (i0 : G) (g : D i0) =>
    Colimit_rec P
      {| legs := legs; legs_comm := legs_comm |}
      (colim i0 g);
  legs_comm :=
    fun (i0 j : G) (g : G i0 j) (x : D i0) =>
    ap
      (Colimit_rec P
         {| legs := legs; legs_comm := legs_comm |})
      (colimp i0 j g x)
|} 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
  {|
    legs :=
      fun (i0 : G) (g0 : D i0) =>
      Colimit_rec P
        {| legs := legs; legs_comm := legs_comm |}
        (colim i0 g0);
    legs_comm :=
      fun (i0 j0 : G) (g0 : G i0 j0) (x0 : D i0) =>
      ap
        (Colimit_rec P
           {| legs := legs; legs_comm := legs_comm |})
        (colimp i0 j0 g0 x0)
  |} 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
  {|
    legs :=
      fun (i0 : G) (g0 : D i0) =>
      Colimit_rec P
        {| legs := legs; legs_comm := legs_comm |}
        (colim i0 g0);
    legs_comm :=
      fun (i0 j0 : G) (g0 : G i0 j0) (x0 : D i0) =>
      ap
        (Colimit_rec P
           {| legs := legs; legs_comm := legs_comm |})
        (colimp i0 j0 g0 x0)
  |} 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
    rewrite Colimit_rec_beta_colimp.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
Cocone.legs_comm
  {| legs := legs; legs_comm := legs_comm |} i j g x @
1 = 1 @ legs_comm i j g x
    hott_simpl. }
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).

(** And we can now show that the HIT is actually a colimit. *)

Definition cocone_colimit {G : Graph} (D : Diagram G) : Cocone D (Colimit D)
  := Build_Cocone colim colimp.

Global 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))
  srapply (isequiv_adjointify _ (Colimit_rec Y) _ _).H: Funext
G: Graph
D: Diagram G
Y: Type
cocone_postcompose (cocone_colimit D) o Colimit_rec Y ==
idmap
H: Funext
G: Graph
D: Diagram G
Y: Type
Colimit_rec Y o cocone_postcompose (cocone_colimit D) ==
idmap
  -H: Funext
G: Graph
D: Diagram G
Y: Type
cocone_postcompose (cocone_colimit D) o Colimit_rec Y ==
idmap intros C.H: Funext
G: Graph
D: Diagram G
Y: Type
C: Cocone D Y
cocone_postcompose (cocone_colimit D)
  (Colimit_rec Y C) = C
    srapply path_cocone.H: Funext
G: Graph
D: Diagram G
Y: Type
C: Cocone D Y
forall i : G,
cocone_postcompose (cocone_colimit D)
  (Colimit_rec Y C) i == C i
H: Funext
G: Graph
D: Diagram G
Y: Type
C: Cocone D Y
forall (i j : G) (g : G i j) (x : D i),
legs_comm
  (cocone_postcompose (cocone_colimit D)
     (Colimit_rec Y C)) i j g x @ ?path_legs i x =
?path_legs j ((D _f g) x) @ legs_comm C i j g x
    1: reflexivity.H: Funext
G: Graph
D: Diagram G
Y: Type
C: Cocone D Y
forall (i j : G) (g : G i j) (x : D i),
legs_comm
  (cocone_postcompose (cocone_colimit D)
     (Colimit_rec Y C)) 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) @
legs_comm C i j g x
    intros i j f x; simpl.H: Funext
G: Graph
D: Diagram G
Y: Type
C: Cocone D Y
i, j: G
f: G i j
x: D i
ap (Colimit_rec Y C) (colimp i j f x) @ 1 =
1 @ legs_comm C i j f x
    apply equiv_p1_1q.H: Funext
G: Graph
D: Diagram G
Y: Type
C: Cocone D Y
i, j: G
f: G i j
x: D i
ap (Colimit_rec Y C) (colimp i j f x) =
legs_comm C i j f x
    apply Colimit_rec_beta_colimp.
  -H: Funext
G: Graph
D: Diagram G
Y: Type
Colimit_rec Y o cocone_postcompose (cocone_colimit D) ==
idmap intro f.H: Funext
G: Graph
D: Diagram G
Y: Type
f: Colimit D -> Y
Colimit_rec Y
  (cocone_postcompose (cocone_colimit D) f) = f
    apply path_forall.H: Funext
G: Graph
D: Diagram G
Y: Type
f: Colimit D -> Y
Colimit_rec Y
  (cocone_postcompose (cocone_colimit D) f) == f
    srapply Colimit_ind.H: Funext
G: Graph
D: Diagram G
Y: Type
f: Colimit D -> Y
forall (i : G) (x : D i),
(fun w : Colimit D =>
 Colimit_rec Y
   (cocone_postcompose (cocone_colimit D) f) w = f w)
  (colim i x)
H: Funext
G: Graph
D: Diagram G
Y: Type
f: Colimit D -> Y
forall (i j : G) (g : G i j) (x : D i),
transport
  (fun w : Colimit D =>
   Colimit_rec Y
     (cocone_postcompose (cocone_colimit D) f) w = 
   f w) (colimp i j g x) (?q j ((D _f g) x)) = ?q i x
    1: reflexivity.H: Funext
G: Graph
D: Diagram G
Y: Type
f: Colimit D -> Y
forall (i j : G) (g : G i j) (x : D i),
transport
  (fun w : Colimit D =>
   Colimit_rec Y
     (cocone_postcompose (cocone_colimit D) f) w = 
   f w) (colimp i j g x)
  ((fun (i0 : G) (x0 : D i0) => 1) j ((D _f g) x)) =
(fun (i0 : G) (x0 : D i0) => 1) i x
    intros i j g x; simpl.H: Funext
G: Graph
D: Diagram G
Y: Type
f: Colimit D -> Y
i, j: G
g: G i j
x: D i
transport
  (fun w : Colimit D =>
   Colimit_rec Y
     (cocone_postcompose (cocone_colimit D) f) w = 
   f w) (colimp i j g x) 1 = 1
    nrapply (transport_paths_FlFr' (g:=f)).H: Funext
G: Graph
D: Diagram G
Y: Type
f: Colimit D -> Y
i, j: G
g: G i j
x: D i
ap
  (Colimit_rec Y
     (cocone_postcompose (cocone_colimit D) f))
  (colimp i j g x) @ 1 = 1 @ ap f (colimp i j g x)
    apply equiv_p1_1q.H: Funext
G: Graph
D: Diagram G
Y: Type
f: Colimit D -> Y
i, j: G
g: G i j
x: D i
ap
  (Colimit_rec Y
     (cocone_postcompose (cocone_colimit D) f))
  (colimp i j g x) = ap f (colimp i j g x)
    apply Colimit_rec_beta_colimp.
Defined.

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

(** * Functoriality of 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) _)^.

  (** ** Colimits of equivalent diagrams *)

  (** Now we have than 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.

  Global 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 particuliar 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.