Cocone.v

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

Local Open Scope path_scope.
Generalizable All Variables.

(** * Cocones *)

(** A Cocone over a diagram [D] to a type [X] is a family of maps from the types of [D] to [X] making the triangles formed with the arrows of [D] commuting. *)

Class Cocone {G : Graph} (D : Diagram G) (X : Type) := {
  legs   : forall i, D i -> X;
  legs_comm  : forall i j (g : G i j), legs j o (D _f g) == legs i;
}.

Arguments Build_Cocone {G D X} legs legs_comm.
Arguments legs {G D X} C i x : rename.
Arguments legs_comm {G D X} C i j g x : rename.

Coercion legs : Cocone >-> Funclass.

Definition issig_Cocone {G : Graph} (D : Diagram G) (X : Type)
  : _ <~> Cocone D X := ltac:(issig).

Section Cocone.
  Context `{Funext} {G : Graph} {D : Diagram G} {X : Type}.

  (** [path_cocone] says when two cocones are equal (up to funext). *)

  Definition path_cocone_naive {C1 C2 : Cocone D X}
    (P := fun q' => forall (i j : G) (g : G i j) (x : D i),
      q' j (D _f g x) = q' i x)
    (path_legs : legs C1 = legs C2)
    (path_legs_comm : transport P path_legs (legs_comm C1) = legs_comm C2)
    : C1 = C2 :=
    match path_legs_comm in (_ = v1)
      return C1 = {|legs := legs C2; legs_comm := v1 |} 
    with
      | idpath => match path_legs in (_ = v0)
        return C1 = {|legs := v0; legs_comm := path_legs # (legs_comm C1) |}
      with
        | idpath => 1
      end
    end.

  Definition path_cocone {C1 C2 : Cocone D X}
    (path_legs : forall i,  C1 i == C2 i)
    (path_legs_comm : forall i j g x,
      legs_comm C1 i j g x @ path_legs i x
      = path_legs j (D _f g x) @ legs_comm C2 i j g x)
    : C1 = C2.H: Funext
G: Graph
D: Diagram G
X: Type
C1, C2: Cocone D X
path_legs: forall i : G, C1 i == C2 i
path_legs_comm: forall (i j : G) (g : G i j)
(x : D i),
legs_comm C1 i j g x @ path_legs i x =
path_legs j ((D _f g) x) @
legs_comm C2 i j g x
C1 = C2
  Proof.H: Funext
G: Graph
D: Diagram G
X: Type
C1, C2: Cocone D X
path_legs: forall i : G, C1 i == C2 i
path_legs_comm: forall (i j : G) (g : G i j)
(x : D i),
legs_comm C1 i j g x @ path_legs i x =
path_legs j ((D _f g) x) @
legs_comm C2 i j g x
C1 = C2
    destruct C1 as [legs pp_q], C2 as [r pp_r].H: Funext
G: Graph
D: Diagram G
X: Type
legs: forall i : G, D i -> X
pp_q: forall (i j : G) (g : G i j),
(fun x : D i => legs j ((D _f g) x)) == legs i
r: forall i : G, D i -> X
pp_r: forall (i j : G) (g : G i j),
(fun x : D i => r j ((D _f g) x)) == r i
path_legs: forall i : G,
{| legs := legs; legs_comm := pp_q |} i ==
{| legs := r; legs_comm := pp_r |} i
path_legs_comm: forall (i j : G) (g : G i j)
(x : D i),
legs_comm
  {|
    legs := legs; legs_comm := pp_q
  |} i j g x @ path_legs i x =
path_legs j ((D _f g) x) @
legs_comm
  {| legs := r; legs_comm := pp_r |}
  i j g x
{| legs := legs; legs_comm := pp_q |} =
{| legs := r; legs_comm := pp_r |}
    refine (path_cocone_naive (path_forall _ _
      (fun i => path_forall _ _ (path_legs i))) _).H: Funext
G: Graph
D: Diagram G
X: Type
legs: forall i : G, D i -> X
pp_q: forall (i j : G) (g : G i j),
(fun x : D i => legs j ((D _f g) x)) == legs i
r: forall i : G, D i -> X
pp_r: forall (i j : G) (g : G i j),
(fun x : D i => r j ((D _f g) x)) == r i
path_legs: forall i : G,
{| legs := legs; legs_comm := pp_q |} i ==
{| legs := r; legs_comm := pp_r |} i
path_legs_comm: forall (i j : G) (g : G i j)
(x : D i),
legs_comm
  {|
    legs := legs; legs_comm := pp_q
  |} i j g x @ path_legs i x =
path_legs j ((D _f g) x) @
legs_comm
  {| legs := r; legs_comm := pp_r |}
  i j g x
transport
  (fun q' : forall x : G, D x -> X =>
   forall (i j : G) (g : G i j) (x : D i),
   q' j ((D _f g) x) = q' i x)
  (path_forall {| legs := legs; legs_comm := pp_q |}
     {| legs := r; legs_comm := pp_r |}
     (fun i : G =>
      path_forall
        ({| legs := legs; legs_comm := pp_q |} i)
        ({| legs := r; legs_comm := pp_r |} i)
        (path_legs i)))
  (legs_comm {| legs := legs; legs_comm := pp_q |}) =
legs_comm {| legs := r; legs_comm := pp_r |}
    cbn; funext i j f x.H: Funext
G: Graph
D: Diagram G
X: Type
legs: forall i : G, D i -> X
pp_q: forall (i j : G) (g : G i j),
(fun x : D i => legs j ((D _f g) x)) == legs i
r: forall i : G, D i -> X
pp_r: forall (i j : G) (g : G i j),
(fun x : D i => r j ((D _f g) x)) == r i
path_legs: forall i : G,
{| legs := legs; legs_comm := pp_q |} i ==
{| legs := r; legs_comm := pp_r |} i
path_legs_comm: forall (i j : G) (g : G i j)
(x : D i),
legs_comm
  {|
    legs := legs; legs_comm := pp_q
  |} i j g x @ path_legs i x =
path_legs j ((D _f g) x) @
legs_comm
  {| legs := r; legs_comm := pp_r |}
  i j g x
i, j: G
f: G i j
x: D i
transport
  (fun q' : forall x : G, D x -> X =>
   forall (i j : G) (g : G i j) (x : D i),
   q' j ((D _f g) x) = q' i x)
  (path_forall legs r
     (fun i : G =>
      path_forall (legs i) (r i) (path_legs i))) pp_q
  i j f x = pp_r i j f x
    rewrite 4 transport_forall_constant, transport_paths_FlFr.H: Funext
G: Graph
D: Diagram G
X: Type
legs: forall i : G, D i -> X
pp_q: forall (i j : G) (g : G i j),
(fun x : D i => legs j ((D _f g) x)) == legs i
r: forall i : G, D i -> X
pp_r: forall (i j : G) (g : G i j),
(fun x : D i => r j ((D _f g) x)) == r i
path_legs: forall i : G,
{| legs := legs; legs_comm := pp_q |} i ==
{| legs := r; legs_comm := pp_r |} i
path_legs_comm: forall (i j : G) (g : G i j)
(x : D i),
legs_comm
  {|
    legs := legs; legs_comm := pp_q
  |} i j g x @ path_legs i x =
path_legs j ((D _f g) x) @
legs_comm
  {| legs := r; legs_comm := pp_r |}
  i j g x
i, j: G
f: G i j
x: D i
((ap
    (fun x0 : forall x : G, D x -> X =>
     x0 j ((D _f f) x))
    (path_forall legs r
       (fun i : G =>
        path_forall (legs i) (r i) (path_legs i))))^ @
 pp_q i j f x) @
ap (fun x0 : forall x : G, D x -> X => x0 i x)
  (path_forall legs r
     (fun i : G =>
      path_forall (legs i) (r i) (path_legs i))) =
pp_r i j f x
    rewrite concat_pp_p; apply moveR_Vp.H: Funext
G: Graph
D: Diagram G
X: Type
legs: forall i : G, D i -> X
pp_q: forall (i j : G) (g : G i j),
(fun x : D i => legs j ((D _f g) x)) == legs i
r: forall i : G, D i -> X
pp_r: forall (i j : G) (g : G i j),
(fun x : D i => r j ((D _f g) x)) == r i
path_legs: forall i : G,
{| legs := legs; legs_comm := pp_q |} i ==
{| legs := r; legs_comm := pp_r |} i
path_legs_comm: forall (i j : G) (g : G i j)
(x : D i),
legs_comm
  {|
    legs := legs; legs_comm := pp_q
  |} i j g x @ path_legs i x =
path_legs j ((D _f g) x) @
legs_comm
  {| legs := r; legs_comm := pp_r |}
  i j g x
i, j: G
f: G i j
x: D i
pp_q i j f x @
ap (fun x0 : forall x : G, D x -> X => x0 i x)
  (path_forall legs r
     (fun i : G =>
      path_forall (legs i) (r i) (path_legs i))) =
ap
  (fun x0 : forall x : G, D x -> X =>
   x0 j ((D _f f) x))
  (path_forall legs r
     (fun i : G =>
      path_forall (legs i) (r i) (path_legs i))) @
pp_r i j f x
    rewrite 2 (ap_apply_lD2 (path_forall _ _
      (fun i => path_forall _ _ (path_legs i)))).H: Funext
G: Graph
D: Diagram G
X: Type
legs: forall i : G, D i -> X
pp_q: forall (i j : G) (g : G i j),
(fun x : D i => legs j ((D _f g) x)) == legs i
r: forall i : G, D i -> X
pp_r: forall (i j : G) (g : G i j),
(fun x : D i => r j ((D _f g) x)) == r i
path_legs: forall i : G,
{| legs := legs; legs_comm := pp_q |} i ==
{| legs := r; legs_comm := pp_r |} i
path_legs_comm: forall (i j : G) (g : G i j)
(x : D i),
legs_comm
  {|
    legs := legs; legs_comm := pp_q
  |} i j g x @ path_legs i x =
path_legs j ((D _f g) x) @
legs_comm
  {| legs := r; legs_comm := pp_r |}
  i j g x
i, j: G
f: G i j
x: D i
pp_q i j f x @
apD10
  (apD10
     (path_forall
        {| legs := legs; legs_comm := pp_q |}
        {| legs := r; legs_comm := pp_r |}
        (fun i : G =>
         path_forall
           ({| legs := legs; legs_comm := pp_q |} i)
           ({| legs := r; legs_comm := pp_r |} i)
           (path_legs i))) i) x =
apD10
  (apD10
     (path_forall
        {| legs := legs; legs_comm := pp_q |}
        {| legs := r; legs_comm := pp_r |}
        (fun i : G =>
         path_forall
           ({| legs := legs; legs_comm := pp_q |} i)
           ({| legs := r; legs_comm := pp_r |} i)
           (path_legs i))) j) ((D _f f) x) @
pp_r i j f x
    rewrite 3 eisretr.H: Funext
G: Graph
D: Diagram G
X: Type
legs: forall i : G, D i -> X
pp_q: forall (i j : G) (g : G i j),
(fun x : D i => legs j ((D _f g) x)) == legs i
r: forall i : G, D i -> X
pp_r: forall (i j : G) (g : G i j),
(fun x : D i => r j ((D _f g) x)) == r i
path_legs: forall i : G,
{| legs := legs; legs_comm := pp_q |} i ==
{| legs := r; legs_comm := pp_r |} i
path_legs_comm: forall (i j : G) (g : G i j)
(x : D i),
legs_comm
  {|
    legs := legs; legs_comm := pp_q
  |} i j g x @ path_legs i x =
path_legs j ((D _f g) x) @
legs_comm
  {| legs := r; legs_comm := pp_r |}
  i j g x
i, j: G
f: G i j
x: D i
pp_q i j f x @ path_legs i x =
path_legs j ((D _f f) x) @ pp_r i j f x
    apply path_legs_comm.
  Defined.

  (** Given a cocone [C] to [X] and a map from [X] to [Y], one can postcompose each map of [C] to get a cocone to [Y]. *)

  Definition cocone_postcompose (C : Cocone D X) {Y : Type}
    : (X -> Y) -> Cocone D Y.H: Funext
G: Graph
D: Diagram G
X: Type
C: Cocone D X
Y: Type
(X -> Y) -> Cocone D Y
  Proof.H: Funext
G: Graph
D: Diagram G
X: Type
C: Cocone D X
Y: Type
(X -> Y) -> Cocone D Y
    intros f.H: Funext
G: Graph
D: Diagram G
X: Type
C: Cocone D X
Y: Type
f: X -> Y
Cocone D Y
    srapply Build_Cocone; intro i.H: Funext
G: Graph
D: Diagram G
X: Type
C: Cocone D X
Y: Type
f: X -> Y
i: G
D i -> Y
H: Funext
G: Graph
D: Diagram G
X: Type
C: Cocone D X
Y: Type
f: X -> Y
i: G
forall (j : G) (g : G i j),
(fun i : G => ?Goal) j o D _f g ==
(fun i : G => ?Goal) i
    1: exact (f o C i).H: Funext
G: Graph
D: Diagram G
X: Type
C: Cocone D X
Y: Type
f: X -> Y
i: G
forall (j : G) (g : G i j),
(fun i : G => f o C i) j o D _f g ==
(fun i : G => f o C i) i
    intros j g x.H: Funext
G: Graph
D: Diagram G
X: Type
C: Cocone D X
Y: Type
f: X -> Y
i, j: G
g: G i j
x: D i
f (C j ((D _f g) x)) = f (C i x)
    exact (ap f (legs_comm _ i j g x)).
  Defined.

  (** ** Universality of a cocone. *)

  (** A colimit will be the extremity of a universal cocone. *)

  (** A cocone [C] over [D] to [X] is said universal when for all [Y] the map [cocone_postcompose] is an equivalence. In particular, given another cocone [C'] over [D] to [X'] the inverse of the map allows to recover a map [h] : [X] -> [X'] such that [C'] is [C] postcomposed with [h]. The fact that [cocone_postcompose] is an equivalence is an elegant way of stating the usual "unique existence" of category theory. *)

  Class UniversalCocone (C : Cocone D X) := {
    is_universal :: forall Y, IsEquiv (@cocone_postcompose C Y);
  }.
  Coercion is_universal : UniversalCocone >-> Funclass.

End Cocone.


(** We now prove several functoriality results, first on cocone and then on colimits. *)

Section FunctorialityCocone.

  Context `{Funext} {G: Graph}.

  (** ** Postcomposition for cocones *)

  (** Identity and associativity for the postcomposition of a cocone with a map. *)

  Definition cocone_postcompose_identity {D : Diagram G} `(C : Cocone _ D X)
    : cocone_postcompose C idmap = C.H: Funext
G: Graph
D: Diagram G
X: Type
C: Cocone D X
cocone_postcompose C idmap = C
  Proof.H: Funext
G: Graph
D: Diagram G
X: Type
C: Cocone D X
cocone_postcompose C idmap = C
    srapply path_cocone; intro i.H: Funext
G: Graph
D: Diagram G
X: Type
C: Cocone D X
i: G
cocone_postcompose C idmap i == C i
H: Funext
G: Graph
D: Diagram G
X: Type
C: Cocone D X
i: G
forall (j : G) (g : G i j) (x : D i),
legs_comm (cocone_postcompose C idmap) i j g x @
(fun i : G => ?Goal) i x =
(fun i : G => ?Goal) j ((D _f g) x) @
legs_comm C i j g x
    1: reflexivity.H: Funext
G: Graph
D: Diagram G
X: Type
C: Cocone D X
i: G
forall (j : G) (g : G i j) (x : D i),
legs_comm (cocone_postcompose C idmap) i j g x @
(fun (i : G) (x0 : D i) => 1) i x =
(fun (i : G) (x0 : D i) => 1) j ((D _f g) x) @
legs_comm C i j g x
    intros j g x; simpl.H: Funext
G: Graph
D: Diagram G
X: Type
C: Cocone D X
i, j: G
g: G i j
x: D i
ap idmap (legs_comm C i j g x) @ 1 =
1 @ legs_comm C i j g x
    apply equiv_p1_1q, ap_idmap.
  Defined.

  Definition cocone_postcompose_comp {D : Diagram G}
             `(f : X -> Y) `(g : Y -> Z) (C : Cocone D X)
    : cocone_postcompose C (g o f)
      = cocone_postcompose (cocone_postcompose C f) g.H: Funext
G: Graph
D: Diagram G
X, Y: Type
f: X -> Y
Z: Type
g: Y -> Z
C: Cocone D X
cocone_postcompose C (g o f) =
cocone_postcompose (cocone_postcompose C f) g
  Proof.H: Funext
G: Graph
D: Diagram G
X, Y: Type
f: X -> Y
Z: Type
g: Y -> Z
C: Cocone D X
cocone_postcompose C (g o f) =
cocone_postcompose (cocone_postcompose C f) g
    srapply path_cocone; intro i.H: Funext
G: Graph
D: Diagram G
X, Y: Type
f: X -> Y
Z: Type
g: Y -> Z
C: Cocone D X
i: G
cocone_postcompose C (g o f) i ==
cocone_postcompose (cocone_postcompose C f) g i
H: Funext
G: Graph
D: Diagram G
X, Y: Type
f: X -> Y
Z: Type
g: Y -> Z
C: Cocone D X
i: G
forall (j : G) (g0 : G i j) (x : D i),
legs_comm (cocone_postcompose C (g o f)) i j g0 x @
(fun i : G => ?Goal) i x =
(fun i : G => ?Goal) j ((D _f g0) x) @
legs_comm
  (cocone_postcompose (cocone_postcompose C f) g) i j
  g0 x
    1: reflexivity.H: Funext
G: Graph
D: Diagram G
X, Y: Type
f: X -> Y
Z: Type
g: Y -> Z
C: Cocone D X
i: G
forall (j : G) (g0 : G i j) (x : D i),
legs_comm (cocone_postcompose C (g o f)) i j g0 x @
(fun (i : G) (x0 : D i) => 1) i x =
(fun (i : G) (x0 : D i) => 1) j ((D _f g0) x) @
legs_comm
  (cocone_postcompose (cocone_postcompose C f) g) i j
  g0 x
    intros j h x; simpl.H: Funext
G: Graph
D: Diagram G
X, Y: Type
f: X -> Y
Z: Type
g: Y -> Z
C: Cocone D X
i, j: G
h: G i j
x: D i
ap (fun x : X => g (f x)) (legs_comm C i j h x) @ 1 =
1 @ ap g (ap f (legs_comm C i j h x))
    apply equiv_p1_1q, ap_compose.
  Defined.

  (** ** Precomposition for cocones *)

  (** Given a cocone over [D2] and a Diagram map [m] : [D1] => [D2], one can precompose each map of the cocone by the corresponding one of [m] to get a cocone over [D1]. *)

  Definition cocone_precompose {D1 D2: Diagram G} (m : DiagramMap D1 D2) {X}
    : (Cocone D2 X) -> (Cocone D1 X).H: Funext
G: Graph
D1, D2: Diagram G
m: DiagramMap D1 D2
X: Type
Cocone D2 X -> Cocone D1 X
  Proof.H: Funext
G: Graph
D1, D2: Diagram G
m: DiagramMap D1 D2
X: Type
Cocone D2 X -> Cocone D1 X
    intro C.H: Funext
G: Graph
D1, D2: Diagram G
m: DiagramMap D1 D2
X: Type
C: Cocone D2 X
Cocone D1 X
    srapply Build_Cocone; intro i.H: Funext
G: Graph
D1, D2: Diagram G
m: DiagramMap D1 D2
X: Type
C: Cocone D2 X
i: G
D1 i -> X
H: Funext
G: Graph
D1, D2: Diagram G
m: DiagramMap D1 D2
X: Type
C: Cocone D2 X
i: G
forall (j : G) (g : G i j),
(fun i : G => ?Goal) j o D1 _f g ==
(fun i : G => ?Goal) i
    1: exact (C i o m i).H: Funext
G: Graph
D1, D2: Diagram G
m: DiagramMap D1 D2
X: Type
C: Cocone D2 X
i: G
forall (j : G) (g : G i j),
(fun i : G => C i o m i) j o D1 _f g ==
(fun i : G => C i o m i) i
    intros j g x; simpl.H: Funext
G: Graph
D1, D2: Diagram G
m: DiagramMap D1 D2
X: Type
C: Cocone D2 X
i, j: G
g: G i j
x: D1 i
C j (m j ((D1 _f g) x)) = C i (m i x)
    etransitivity.H: Funext
G: Graph
D1, D2: Diagram G
m: DiagramMap D1 D2
X: Type
C: Cocone D2 X
i, j: G
g: G i j
x: D1 i
C j (m j ((D1 _f g) x)) = ?Goal
H: Funext
G: Graph
D1, D2: Diagram G
m: DiagramMap D1 D2
X: Type
C: Cocone D2 X
i, j: G
g: G i j
x: D1 i
?Goal = C i (m i x)
    +H: Funext
G: Graph
D1, D2: Diagram G
m: DiagramMap D1 D2
X: Type
C: Cocone D2 X
i, j: G
g: G i j
x: D1 i
C j (m j ((D1 _f g) x)) = ?Goal apply ap.H: Funext
G: Graph
D1, D2: Diagram G
m: DiagramMap D1 D2
X: Type
C: Cocone D2 X
i, j: G
g: G i j
x: D1 i
m j ((D1 _f g) x) = ?y
      symmetry.H: Funext
G: Graph
D1, D2: Diagram G
m: DiagramMap D1 D2
X: Type
C: Cocone D2 X
i, j: G
g: G i j
x: D1 i
?y = m j ((D1 _f g) x)
      apply DiagramMap_comm.
    +H: Funext
G: Graph
D1, D2: Diagram G
m: DiagramMap D1 D2
X: Type
C: Cocone D2 X
i, j: G
g: G i j
x: D1 i
C j ((D2 _f g) (m i x)) = C i (m i x) apply legs_comm.
  Defined.

  (** Identity and associativity for the precomposition of a cocone with a diagram map. *)

  Definition cocone_precompose_identity (D : Diagram G) (X : Type)
    : cocone_precompose (X:=X) (diagram_idmap D) == idmap.H: Funext
G: Graph
D: Diagram G
X: Type
cocone_precompose (diagram_idmap D) == idmap
  Proof.H: Funext
G: Graph
D: Diagram G
X: Type
cocone_precompose (diagram_idmap D) == idmap
    intro C; srapply path_cocone; simpl.H: Funext
G: Graph
D: Diagram G
X: Type
C: Cocone D X
forall i : G, (fun x : D i => C i x) == C i
H: Funext
G: Graph
D: Diagram G
X: Type
C: Cocone D X
forall (i j : G) (g : G i j) (x : D i),
(1 @ legs_comm C i j g x) @ ?Goal i x =
?Goal j ((D _f g) x) @ legs_comm C i j g x
    1: reflexivity.H: Funext
G: Graph
D: Diagram G
X: Type
C: Cocone D X
forall (i j : G) (g : G i j) (x : D i),
(1 @ legs_comm 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; simpl.H: Funext
G: Graph
D: Diagram G
X: Type
C: Cocone D X
i, j: G
g: G i j
x: D i
(1 @ legs_comm C i j g x) @ 1 =
1 @ legs_comm C i j g x
    apply concat_p1.
  Defined.

  Definition cocone_precompose_comp {D1 D2 D3 : Diagram G}
    (m2 : DiagramMap D2 D3) (m1 : DiagramMap D1 D2) (X : Type)
    : (cocone_precompose (X:=X) m1) o (cocone_precompose m2)
      == cocone_precompose (diagram_comp m2 m1).H: Funext
G: Graph
D1, D2, D3: Diagram G
m2: DiagramMap D2 D3
m1: DiagramMap D1 D2
X: Type
cocone_precompose m1 o cocone_precompose m2 ==
cocone_precompose (diagram_comp m2 m1)
  Proof.H: Funext
G: Graph
D1, D2, D3: Diagram G
m2: DiagramMap D2 D3
m1: DiagramMap D1 D2
X: Type
cocone_precompose m1 o cocone_precompose m2 ==
cocone_precompose (diagram_comp m2 m1)
    intro C; simpl.H: Funext
G: Graph
D1, D2, D3: Diagram G
m2: DiagramMap D2 D3
m1: DiagramMap D1 D2
X: Type
C: Cocone D3 X
cocone_precompose m1 (cocone_precompose m2 C) =
cocone_precompose (diagram_comp m2 m1) C
    srapply path_cocone.H: Funext
G: Graph
D1, D2, D3: Diagram G
m2: DiagramMap D2 D3
m1: DiagramMap D1 D2
X: Type
C: Cocone D3 X
forall i : G,
cocone_precompose m1 (cocone_precompose m2 C) i ==
cocone_precompose (diagram_comp m2 m1) C i
H: Funext
G: Graph
D1, D2, D3: Diagram G
m2: DiagramMap D2 D3
m1: DiagramMap D1 D2
X: Type
C: Cocone D3 X
forall (i j : G) (g : G i j) (x : D1 i),
legs_comm
  (cocone_precompose m1 (cocone_precompose m2 C)) i j
  g x @ ?path_legs i x =
?path_legs j ((D1 _f g) x) @
legs_comm (cocone_precompose (diagram_comp m2 m1) C) i
  j g x
    1: reflexivity.H: Funext
G: Graph
D1, D2, D3: Diagram G
m2: DiagramMap D2 D3
m1: DiagramMap D1 D2
X: Type
C: Cocone D3 X
forall (i j : G) (g : G i j) (x : D1 i),
legs_comm
  (cocone_precompose m1 (cocone_precompose m2 C)) i j
  g x @ (fun (i0 : G) (x0 : D1 i0) => 1) i x =
(fun (i0 : G) (x0 : D1 i0) => 1) j ((D1 _f g) x) @
legs_comm (cocone_precompose (diagram_comp m2 m1) C) i
  j g x
    intros i j g x; simpl.H: Funext
G: Graph
D1, D2, D3: Diagram G
m2: DiagramMap D2 D3
m1: DiagramMap D1 D2
X: Type
C: Cocone D3 X
i, j: G
g: G i j
x: D1 i
(ap (fun x : D2 j => C j (m2 j x))
   (DiagramMap_comm m1 g x)^ @
 (ap (C j) (DiagramMap_comm m2 g (m1 i x))^ @
  legs_comm C i j g (m2 i (m1 i x)))) @ 1 =
1 @
(ap (C j)
   (CommutativeSquares.comm_square_comp
      (DiagramMap_comm m1 g) (DiagramMap_comm m2 g) x)^ @
 legs_comm C i j g (m2 i (m1 i x)))
    apply equiv_p1_1q.H: Funext
G: Graph
D1, D2, D3: Diagram G
m2: DiagramMap D2 D3
m1: DiagramMap D1 D2
X: Type
C: Cocone D3 X
i, j: G
g: G i j
x: D1 i
ap (fun x : D2 j => C j (m2 j x))
  (DiagramMap_comm m1 g x)^ @
(ap (C j) (DiagramMap_comm m2 g (m1 i x))^ @
 legs_comm C i j g (m2 i (m1 i x))) =
ap (C j)
  (CommutativeSquares.comm_square_comp
     (DiagramMap_comm m1 g) (DiagramMap_comm m2 g) x)^ @
legs_comm C i j g (m2 i (m1 i x))
    unfold CommutativeSquares.comm_square_comp.H: Funext
G: Graph
D1, D2, D3: Diagram G
m2: DiagramMap D2 D3
m1: DiagramMap D1 D2
X: Type
C: Cocone D3 X
i, j: G
g: G i j
x: D1 i
ap (fun x : D2 j => C j (m2 j x))
  (DiagramMap_comm m1 g x)^ @
(ap (C j) (DiagramMap_comm m2 g (m1 i x))^ @
 legs_comm C i j g (m2 i (m1 i x))) =
ap (C j)
  (DiagramMap_comm m2 g (m1 i x) @
   ap (m2 j) (DiagramMap_comm m1 g x))^ @
legs_comm C i j g (m2 i (m1 i x))
    refine (concat_p_pp _ _ _ @ _).H: Funext
G: Graph
D1, D2, D3: Diagram G
m2: DiagramMap D2 D3
m1: DiagramMap D1 D2
X: Type
C: Cocone D3 X
i, j: G
g: G i j
x: D1 i
(ap (fun x : D2 j => C j (m2 j x))
   (DiagramMap_comm m1 g x)^ @
 ap (C j) (DiagramMap_comm m2 g (m1 i x))^) @
legs_comm C i j g (m2 i (m1 i x)) =
ap (C j)
  (DiagramMap_comm m2 g (m1 i x) @
   ap (m2 j) (DiagramMap_comm m1 g x))^ @
legs_comm C i j g (m2 i (m1 i x))
    apply ap10, ap.H: Funext
G: Graph
D1, D2, D3: Diagram G
m2: DiagramMap D2 D3
m1: DiagramMap D1 D2
X: Type
C: Cocone D3 X
i, j: G
g: G i j
x: D1 i
ap (fun x : D2 j => C j (m2 j x))
  (DiagramMap_comm m1 g x)^ @
ap (C j) (DiagramMap_comm m2 g (m1 i x))^ =
ap (C j)
  (DiagramMap_comm m2 g (m1 i x) @
   ap (m2 j) (DiagramMap_comm m1 g x))^
    rewrite 3 ap_V.H: Funext
G: Graph
D1, D2, D3: Diagram G
m2: DiagramMap D2 D3
m1: DiagramMap D1 D2
X: Type
C: Cocone D3 X
i, j: G
g: G i j
x: D1 i
(ap (fun x : D2 j => C j (m2 j x))
   (DiagramMap_comm m1 g x))^ @
(ap (C j) (DiagramMap_comm m2 g (m1 i x)))^ =
(ap (C j)
   (DiagramMap_comm m2 g (m1 i x) @
    ap (m2 j) (DiagramMap_comm m1 g x)))^
    refine ((inv_pp _ _)^ @ _).H: Funext
G: Graph
D1, D2, D3: Diagram G
m2: DiagramMap D2 D3
m1: DiagramMap D1 D2
X: Type
C: Cocone D3 X
i, j: G
g: G i j
x: D1 i
(ap (C j) (DiagramMap_comm m2 g (m1 i x)) @
 ap (fun x : D2 j => C j (m2 j x))
   (DiagramMap_comm m1 g x))^ =
(ap (C j)
   (DiagramMap_comm m2 g (m1 i x) @
    ap (m2 j) (DiagramMap_comm m1 g x)))^
    apply inverse2.H: Funext
G: Graph
D1, D2, D3: Diagram G
m2: DiagramMap D2 D3
m1: DiagramMap D1 D2
X: Type
C: Cocone D3 X
i, j: G
g: G i j
x: D1 i
ap (C j) (DiagramMap_comm m2 g (m1 i x)) @
ap (fun x : D2 j => C j (m2 j x))
  (DiagramMap_comm m1 g x) =
ap (C j)
  (DiagramMap_comm m2 g (m1 i x) @
   ap (m2 j) (DiagramMap_comm m1 g x))
    rewrite ap_pp.H: Funext
G: Graph
D1, D2, D3: Diagram G
m2: DiagramMap D2 D3
m1: DiagramMap D1 D2
X: Type
C: Cocone D3 X
i, j: G
g: G i j
x: D1 i
ap (C j) (DiagramMap_comm m2 g (m1 i x)) @
ap (fun x : D2 j => C j (m2 j x))
  (DiagramMap_comm m1 g x) =
ap (C j) (DiagramMap_comm m2 g (m1 i x)) @
ap (C j) (ap (m2 j) (DiagramMap_comm m1 g x))
    apply ap.H: Funext
G: Graph
D1, D2, D3: Diagram G
m2: DiagramMap D2 D3
m1: DiagramMap D1 D2
X: Type
C: Cocone D3 X
i, j: G
g: G i j
x: D1 i
ap (fun x : D2 j => C j (m2 j x))
  (DiagramMap_comm m1 g x) =
ap (C j) (ap (m2 j) (DiagramMap_comm m1 g x))
    by rewrite ap_compose.
  Defined.

  (** Associativity of a precomposition and a postcomposition. *)

  Definition cocone_precompose_postcompose {D1 D2 : Diagram G}
             (m : DiagramMap D1 D2) `(f : X -> Y) (C : Cocone D2 X)
    : cocone_postcompose (cocone_precompose m C) f
      = cocone_precompose m (cocone_postcompose C f).H: Funext
G: Graph
D1, D2: Diagram G
m: DiagramMap D1 D2
X, Y: Type
f: X -> Y
C: Cocone D2 X
cocone_postcompose (cocone_precompose m C) f =
cocone_precompose m (cocone_postcompose C f)
  Proof.H: Funext
G: Graph
D1, D2: Diagram G
m: DiagramMap D1 D2
X, Y: Type
f: X -> Y
C: Cocone D2 X
cocone_postcompose (cocone_precompose m C) f =
cocone_precompose m (cocone_postcompose C f)
    srapply path_cocone; intro i.H: Funext
G: Graph
D1, D2: Diagram G
m: DiagramMap D1 D2
X, Y: Type
f: X -> Y
C: Cocone D2 X
i: G
cocone_postcompose (cocone_precompose m C) f i ==
cocone_precompose m (cocone_postcompose C f) i
H: Funext
G: Graph
D1, D2: Diagram G
m: DiagramMap D1 D2
X, Y: Type
f: X -> Y
C: Cocone D2 X
i: G
forall (j : G) (g : G i j) (x : D1 i),
legs_comm
  (cocone_postcompose (cocone_precompose m C) f) i j g
  x @ (fun i : G => ?Goal) i x =
(fun i : G => ?Goal) j ((D1 _f g) x) @
legs_comm
  (cocone_precompose m (cocone_postcompose C f)) i j g
  x
    1: reflexivity.H: Funext
G: Graph
D1, D2: Diagram G
m: DiagramMap D1 D2
X, Y: Type
f: X -> Y
C: Cocone D2 X
i: G
forall (j : G) (g : G i j) (x : D1 i),
legs_comm
  (cocone_postcompose (cocone_precompose m C) f) i j g
  x @ (fun (i : G) (x0 : D1 i) => 1) i x =
(fun (i : G) (x0 : D1 i) => 1) j ((D1 _f g) x) @
legs_comm
  (cocone_precompose m (cocone_postcompose C f)) i j g
  x
    intros j g x; simpl.H: Funext
G: Graph
D1, D2: Diagram G
m: DiagramMap D1 D2
X, Y: Type
f: X -> Y
C: Cocone D2 X
i, j: G
g: G i j
x: D1 i
ap f
  (ap (C j) (DiagramMap_comm m g x)^ @
   legs_comm C i j g (m i x)) @ 1 =
1 @
(ap (fun x : D2 j => f (C j x))
   (DiagramMap_comm m g x)^ @
 ap f (legs_comm C i j g (m i x)))
    apply equiv_p1_1q.H: Funext
G: Graph
D1, D2: Diagram G
m: DiagramMap D1 D2
X, Y: Type
f: X -> Y
C: Cocone D2 X
i, j: G
g: G i j
x: D1 i
ap f
  (ap (C j) (DiagramMap_comm m g x)^ @
   legs_comm C i j g (m i x)) =
ap (fun x : D2 j => f (C j x))
  (DiagramMap_comm m g x)^ @
ap f (legs_comm C i j g (m i x))
    etransitivity.H: Funext
G: Graph
D1, D2: Diagram G
m: DiagramMap D1 D2
X, Y: Type
f: X -> Y
C: Cocone D2 X
i, j: G
g: G i j
x: D1 i
ap f
  (ap (C j) (DiagramMap_comm m g x)^ @
   legs_comm C i j g (m i x)) = ?Goal
H: Funext
G: Graph
D1, D2: Diagram G
m: DiagramMap D1 D2
X, Y: Type
f: X -> Y
C: Cocone D2 X
i, j: G
g: G i j
x: D1 i
?Goal =
ap (fun x : D2 j => f (C j x))
  (DiagramMap_comm m g x)^ @
ap f (legs_comm C i j g (m i x))
    +H: Funext
G: Graph
D1, D2: Diagram G
m: DiagramMap D1 D2
X, Y: Type
f: X -> Y
C: Cocone D2 X
i, j: G
g: G i j
x: D1 i
ap f
  (ap (C j) (DiagramMap_comm m g x)^ @
   legs_comm C i j g (m i x)) = ?Goal apply ap_pp.
    +H: Funext
G: Graph
D1, D2: Diagram G
m: DiagramMap D1 D2
X, Y: Type
f: X -> Y
C: Cocone D2 X
i, j: G
g: G i j
x: D1 i
ap f (ap (C j) (DiagramMap_comm m g x)^) @
ap f (legs_comm C i j g (m i x)) =
ap (fun x : D2 j => f (C j x))
  (DiagramMap_comm m g x)^ @
ap f (legs_comm C i j g (m i x)) apply ap10, ap.H: Funext
G: Graph
D1, D2: Diagram G
m: DiagramMap D1 D2
X, Y: Type
f: X -> Y
C: Cocone D2 X
i, j: G
g: G i j
x: D1 i
ap f (ap (C j) (DiagramMap_comm m g x)^) =
ap (fun x : D2 j => f (C j x))
  (DiagramMap_comm m g x)^
      symmetry.H: Funext
G: Graph
D1, D2: Diagram G
m: DiagramMap D1 D2
X, Y: Type
f: X -> Y
C: Cocone D2 X
i, j: G
g: G i j
x: D1 i
ap (fun x : D2 j => f (C j x))
  (DiagramMap_comm m g x)^ =
ap f (ap (C j) (DiagramMap_comm m g x)^)
      apply ap_compose.
  Defined.

  (** The precomposition with a diagram equivalence is an equivalence. *)

  #[export] Instance cocone_precompose_equiv {D1 D2 : Diagram G}
    (m : D1 ~d~ D2) (X : Type) : IsEquiv (cocone_precompose (X:=X) m).H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
X: Type
IsEquiv (cocone_precompose m)
  Proof.H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
X: Type
IsEquiv (cocone_precompose m)
    srapply isequiv_adjointify.H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
X: Type
Cocone D1 X -> Cocone D2 X
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
X: Type
cocone_precompose m o ?g == idmap
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
X: Type
?g o cocone_precompose m == idmap
    1: exact (cocone_precompose (diagram_equiv_inv m)).H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
X: Type
cocone_precompose m
o cocone_precompose (diagram_equiv_inv m) == idmap
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
X: Type
cocone_precompose (diagram_equiv_inv m)
o cocone_precompose m == idmap
    +H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
X: Type
cocone_precompose m
o cocone_precompose (diagram_equiv_inv m) == idmap intros C.H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
X: Type
C: Cocone D1 X
cocone_precompose m
  (cocone_precompose (diagram_equiv_inv m) C) = C
      etransitivity.H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
X: Type
C: Cocone D1 X
cocone_precompose m
  (cocone_precompose (diagram_equiv_inv m) C) = ?Goal
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
X: Type
C: Cocone D1 X
?Goal = C
      -H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
X: Type
C: Cocone D1 X
cocone_precompose m
  (cocone_precompose (diagram_equiv_inv m) C) = ?Goal apply cocone_precompose_comp.
      -H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
X: Type
C: Cocone D1 X
cocone_precompose
  (diagram_comp (diagram_equiv_inv m) m) C = C rewrite diagram_inv_is_retraction.H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
X: Type
C: Cocone D1 X
cocone_precompose (diagram_idmap D1) C = C
        apply cocone_precompose_identity.
    +H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
X: Type
cocone_precompose (diagram_equiv_inv m)
o cocone_precompose m == idmap intros C.H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
X: Type
C: Cocone D2 X
cocone_precompose (diagram_equiv_inv m)
  (cocone_precompose m C) = C
      etransitivity.H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
X: Type
C: Cocone D2 X
cocone_precompose (diagram_equiv_inv m)
  (cocone_precompose m C) = ?Goal
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
X: Type
C: Cocone D2 X
?Goal = C
      -H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
X: Type
C: Cocone D2 X
cocone_precompose (diagram_equiv_inv m)
  (cocone_precompose m C) = ?Goal apply cocone_precompose_comp.
      -H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
X: Type
C: Cocone D2 X
cocone_precompose
  (diagram_comp m (diagram_equiv_inv m)) C = C rewrite diagram_inv_is_section.H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
X: Type
C: Cocone D2 X
cocone_precompose (diagram_idmap D2) C = C
        apply cocone_precompose_identity.
  Defined.

  (** The postcomposition with an equivalence is an equivalence. *)

  #[export] Instance cocone_postcompose_equiv {D : Diagram G} `(f : X <~> Y)
    : IsEquiv (fun C : Cocone D X => cocone_postcompose C f).H: Funext
G: Graph
D: Diagram G
X, Y: Type
f: X <~> Y
IsEquiv (fun C : Cocone D X => cocone_postcompose C f)
  Proof.H: Funext
G: Graph
D: Diagram G
X, Y: Type
f: X <~> Y
IsEquiv (fun C : Cocone D X => cocone_postcompose C f)
    srapply isequiv_adjointify.H: Funext
G: Graph
D: Diagram G
X, Y: Type
f: X <~> Y
Cocone D Y -> Cocone D X
H: Funext
G: Graph
D: Diagram G
X, Y: Type
f: X <~> Y
(fun C : Cocone D X => cocone_postcompose C f) o ?g ==
idmap
H: Funext
G: Graph
D: Diagram G
X, Y: Type
f: X <~> Y
?g o (fun C : Cocone D X => cocone_postcompose C f) ==
idmap
    1: exact (fun C => cocone_postcompose C f^-1).H: Funext
G: Graph
D: Diagram G
X, Y: Type
f: X <~> Y
(fun C : Cocone D X => cocone_postcompose C f)
o (fun C : Cocone D Y => cocone_postcompose C f^-1) ==
idmap
H: Funext
G: Graph
D: Diagram G
X, Y: Type
f: X <~> Y
(fun C : Cocone D Y => cocone_postcompose C f^-1)
o (fun C : Cocone D X => cocone_postcompose C f) ==
idmap
    +H: Funext
G: Graph
D: Diagram G
X, Y: Type
f: X <~> Y
(fun C : Cocone D X => cocone_postcompose C f)
o (fun C : Cocone D Y => cocone_postcompose C f^-1) ==
idmap intros C.H: Funext
G: Graph
D: Diagram G
X, Y: Type
f: X <~> Y
C: Cocone D Y
cocone_postcompose (cocone_postcompose C f^-1) f = C
      etransitivity.H: Funext
G: Graph
D: Diagram G
X, Y: Type
f: X <~> Y
C: Cocone D Y
cocone_postcompose (cocone_postcompose C f^-1) f =
?Goal
H: Funext
G: Graph
D: Diagram G
X, Y: Type
f: X <~> Y
C: Cocone D Y
?Goal = C
      -H: Funext
G: Graph
D: Diagram G
X, Y: Type
f: X <~> Y
C: Cocone D Y
cocone_postcompose (cocone_postcompose C f^-1) f =
?Goal symmetry.H: Funext
G: Graph
D: Diagram G
X, Y: Type
f: X <~> Y
C: Cocone D Y
?Goal =
cocone_postcompose (cocone_postcompose C f^-1) f
        apply cocone_postcompose_comp.
      -H: Funext
G: Graph
D: Diagram G
X, Y: Type
f: X <~> Y
C: Cocone D Y
cocone_postcompose C (fun x : Y => f (f^-1 x)) = C etransitivity.H: Funext
G: Graph
D: Diagram G
X, Y: Type
f: X <~> Y
C: Cocone D Y
cocone_postcompose C (fun x : Y => f (f^-1 x)) = ?Goal
H: Funext
G: Graph
D: Diagram G
X, Y: Type
f: X <~> Y
C: Cocone D Y
?Goal = C
        2: apply cocone_postcompose_identity.H: Funext
G: Graph
D: Diagram G
X, Y: Type
f: X <~> Y
C: Cocone D Y
cocone_postcompose C (fun x : Y => f (f^-1 x)) =
cocone_postcompose C idmap
        apply ap.H: Funext
G: Graph
D: Diagram G
X, Y: Type
f: X <~> Y
C: Cocone D Y
(fun x : Y => f (f^-1 x)) = idmap
        funext x; apply eisretr.
    +H: Funext
G: Graph
D: Diagram G
X, Y: Type
f: X <~> Y
(fun C : Cocone D Y => cocone_postcompose C f^-1)
o (fun C : Cocone D X => cocone_postcompose C f) ==
idmap intros C.H: Funext
G: Graph
D: Diagram G
X, Y: Type
f: X <~> Y
C: Cocone D X
cocone_postcompose (cocone_postcompose C f) f^-1 = C
      etransitivity.H: Funext
G: Graph
D: Diagram G
X, Y: Type
f: X <~> Y
C: Cocone D X
cocone_postcompose (cocone_postcompose C f) f^-1 =
?Goal
H: Funext
G: Graph
D: Diagram G
X, Y: Type
f: X <~> Y
C: Cocone D X
?Goal = C
      -H: Funext
G: Graph
D: Diagram G
X, Y: Type
f: X <~> Y
C: Cocone D X
cocone_postcompose (cocone_postcompose C f) f^-1 =
?Goal symmetry.H: Funext
G: Graph
D: Diagram G
X, Y: Type
f: X <~> Y
C: Cocone D X
?Goal =
cocone_postcompose (cocone_postcompose C f) f^-1
        apply cocone_postcompose_comp.
      -H: Funext
G: Graph
D: Diagram G
X, Y: Type
f: X <~> Y
C: Cocone D X
cocone_postcompose C (fun x : X => f^-1 (f x)) = C etransitivity.H: Funext
G: Graph
D: Diagram G
X, Y: Type
f: X <~> Y
C: Cocone D X
cocone_postcompose C (fun x : X => f^-1 (f x)) = ?Goal
H: Funext
G: Graph
D: Diagram G
X, Y: Type
f: X <~> Y
C: Cocone D X
?Goal = C
        2: apply cocone_postcompose_identity.H: Funext
G: Graph
D: Diagram G
X, Y: Type
f: X <~> Y
C: Cocone D X
cocone_postcompose C (fun x : X => f^-1 (f x)) =
cocone_postcompose C idmap
        apply ap.H: Funext
G: Graph
D: Diagram G
X, Y: Type
f: X <~> Y
C: Cocone D X
(fun x : X => f^-1 (f x)) = idmap
        funext x; apply eissect.
  Defined.

  (** ** Universality preservation *)

  (** Universality of a cocone is preserved by composition with a (diagram) equivalence. *)

  #[export] Instance cocone_precompose_equiv_universality {D1 D2 : Diagram G}
    (m: D1 ~d~ D2) {X} (C : Cocone D2 X) (_ : UniversalCocone C)
    : UniversalCocone (cocone_precompose (X:=X) m C).H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
X: Type
C: Cocone D2 X
X0: UniversalCocone C
UniversalCocone (cocone_precompose m C)
  Proof.H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
X: Type
C: Cocone D2 X
X0: UniversalCocone C
UniversalCocone (cocone_precompose m C)
    srapply Build_UniversalCocone; intro.H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
X: Type
C: Cocone D2 X
X0: UniversalCocone C
Y: Type
IsEquiv (cocone_postcompose (cocone_precompose m C))
    rewrite (path_forall _ _ (fun f => cocone_precompose_postcompose m f C)).H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
X: Type
C: Cocone D2 X
X0: UniversalCocone C
Y: Type
IsEquiv
  (fun f : X -> Y =>
   cocone_precompose m (cocone_postcompose C f))
    rapply isequiv_compose.
  Defined.

  #[export] Instance cocone_postcompose_equiv_universality {D: Diagram G} `(f: X <~> Y)
    (C : Cocone D X) (_ : UniversalCocone C)
    : UniversalCocone (cocone_postcompose C f).H: Funext
G: Graph
D: Diagram G
X, Y: Type
f: X <~> Y
C: Cocone D X
X0: UniversalCocone C
UniversalCocone (cocone_postcompose C f)
  Proof.H: Funext
G: Graph
D: Diagram G
X, Y: Type
f: X <~> Y
C: Cocone D X
X0: UniversalCocone C
UniversalCocone (cocone_postcompose C f)
    snapply Build_UniversalCocone; intro.H: Funext
G: Graph
D: Diagram G
X, Y: Type
f: X <~> Y
C: Cocone D X
X0: UniversalCocone C
Y0: Type
IsEquiv (cocone_postcompose (cocone_postcompose C f))
    rewrite <- (path_forall _ _ (fun g => cocone_postcompose_comp f g C)).H: Funext
G: Graph
D: Diagram G
X, Y: Type
f: X <~> Y
C: Cocone D X
X0: UniversalCocone C
Y0: Type
IsEquiv
  (fun g : Y -> Y0 =>
   cocone_postcompose C (fun x : X => g (f x)))
    rapply isequiv_compose.
  Defined.

End FunctorialityCocone.