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.

(** * Cones *)

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

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

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

Coercion legs : Cone >-> Funclass.

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

  (** [path_cone] says when two cones are equals (up to funext). *)

  Definition path_cocone_naive {C1 C2 : Cone X D}
    (P := fun q' => forall (i j : G) (g : G i j) (x : X),
      D _f g (q' i x) = q' j 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_cone {C1 C2 : Cone X D}
    (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 j x
      = ap (D _f g) (path_legs i x) @ legs_comm C2 i j g x)
    : C1 = C2.
H: Funext
X: Type
G: Graph
D: Diagram G
C1, C2: Cone X D
path_legs: forall i : G, C1 i == C2 i
path_legs_comm: forall (i j : G) (g : G i j) 
(x : X),
legs_comm C1 i j g x @ path_legs j x =
ap (D _f g) (path_legs i x) @
legs_comm C2 i j g x
C1 = C2
  Proof.
H: Funext
X: Type
G: Graph
D: Diagram G
C1, C2: Cone X D
path_legs: forall i : G, C1 i == C2 i
path_legs_comm: forall (i j : G) (g : G i j) 
(x : X),
legs_comm C1 i j g x @ path_legs j x =
ap (D _f g) (path_legs i x) @
legs_comm C2 i j g x
C1 = C2
    destruct C1 as [legs pp_q], C2 as [r pp_r].
H: Funext
X: Type
G: Graph
D: Diagram G
legs: forall i : G, X -> D i
pp_q: forall (i j : G) (g : G i j),
(fun x : X => (D _f g) (legs i x)) == legs j
r: forall i : G, X -> D i
pp_r: forall (i j : G) (g : G i j),
(fun x : X => (D _f g) (r i x)) == r j
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 : X),
legs_comm
  {|
    legs := legs; legs_comm := pp_q
  |} i j g x @ path_legs j x =
ap (D _f g) (path_legs i 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
X: Type
G: Graph
D: Diagram G
legs: forall i : G, X -> D i
pp_q: forall (i j : G) (g : G i j),
(fun x : X => (D _f g) (legs i x)) == legs j
r: forall i : G, X -> D i
pp_r: forall (i j : G) (g : G i j),
(fun x : X => (D _f g) (r i x)) == r j
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 : X),
legs_comm
  {|
    legs := legs; legs_comm := pp_q
  |} i j g x @ path_legs j x =
ap (D _f g) (path_legs i x) @
legs_comm
  {| legs := r; legs_comm := pp_r |}
  i j g x
transport
  (fun q' : forall x : G, X -> D x =>
   forall (i j : G) (g : G i j) (x : X),
   (D _f g) (q' i x) = q' j 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
X: Type
G: Graph
D: Diagram G
legs: forall i : G, X -> D i
pp_q: forall (i j : G) (g : G i j),
(fun x : X => (D _f g) (legs i x)) == legs j
r: forall i : G, X -> D i
pp_r: forall (i j : G) (g : G i j),
(fun x : X => (D _f g) (r i x)) == r j
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 : X),
legs_comm
  {|
    legs := legs; legs_comm := pp_q
  |} i j g x @ path_legs j x =
ap (D _f g) (path_legs i x) @
legs_comm
  {| legs := r; legs_comm := pp_r |}
  i j g x
i, j: G
f: G i j
x: X
transport
  (fun q' : forall x : G, X -> D x =>
   forall (i j : G) (g : G i j) (x : X),
   (D _f g) (q' i x) = q' j 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
X: Type
G: Graph
D: Diagram G
legs: forall i : G, X -> D i
pp_q: forall (i j : G) (g : G i j),
(fun x : X => (D _f g) (legs i x)) == legs j
r: forall i : G, X -> D i
pp_r: forall (i j : G) (g : G i j),
(fun x : X => (D _f g) (r i x)) == r j
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 : X),
legs_comm
  {|
    legs := legs; legs_comm := pp_q
  |} i j g x @ path_legs j x =
ap (D _f g) (path_legs i x) @
legs_comm
  {| legs := r; legs_comm := pp_r |}
  i j g x
i, j: G
f: G i j
x: X
((ap
    (fun x0 : forall x : G, X -> D x =>
     (D _f f) (x0 i 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, X -> D x => x0 j 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
X: Type
G: Graph
D: Diagram G
legs: forall i : G, X -> D i
pp_q: forall (i j : G) (g : G i j),
(fun x : X => (D _f g) (legs i x)) == legs j
r: forall i : G, X -> D i
pp_r: forall (i j : G) (g : G i j),
(fun x : X => (D _f g) (r i x)) == r j
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 : X),
legs_comm
  {|
    legs := legs; legs_comm := pp_q
  |} i j g x @ path_legs j x =
ap (D _f g) (path_legs i x) @
legs_comm
  {| legs := r; legs_comm := pp_r |}
  i j g x
i, j: G
f: G i j
x: X
pp_q i j f x @
ap (fun x0 : forall x : G, X -> D x => x0 j x)
  (path_forall legs r
     (fun i : G =>
      path_forall (legs i) (r i) (path_legs i))) =
ap
  (fun x0 : forall x : G, X -> D x =>
   (D _f f) (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 ap_compose.
H: Funext
X: Type
G: Graph
D: Diagram G
legs: forall i : G, X -> D i
pp_q: forall (i j : G) (g : G i j),
(fun x : X => (D _f g) (legs i x)) == legs j
r: forall i : G, X -> D i
pp_r: forall (i j : G) (g : G i j),
(fun x : X => (D _f g) (r i x)) == r j
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 : X),
legs_comm
  {|
    legs := legs; legs_comm := pp_q
  |} i j g x @ path_legs j x =
ap (D _f g) (path_legs i x) @
legs_comm
  {| legs := r; legs_comm := pp_r |}
  i j g x
i, j: G
f: G i j
x: X
pp_q i j f x @
ap (fun x0 : forall x : G, X -> D x => x0 j x)
  (path_forall legs r
     (fun i : G =>
      path_forall (legs i) (r i) (path_legs i))) =
ap (D _f f)
  (ap (fun x0 : forall x : G, X -> D 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 2 (ap_apply_lD2 (path_forall legs r
      (fun i => path_forall (legs i) (r i) (path_legs i)))).
H: Funext
X: Type
G: Graph
D: Diagram G
legs: forall i : G, X -> D i
pp_q: forall (i j : G) (g : G i j),
(fun x : X => (D _f g) (legs i x)) == legs j
r: forall i : G, X -> D i
pp_r: forall (i j : G) (g : G i j),
(fun x : X => (D _f g) (r i x)) == r j
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 : X),
legs_comm
  {|
    legs := legs; legs_comm := pp_q
  |} i j g x @ path_legs j x =
ap (D _f g) (path_legs i x) @
legs_comm
  {| legs := r; legs_comm := pp_r |}
  i j g x
i, j: G
f: G i j
x: X
pp_q i j f x @
apD10
  (apD10
     (path_forall legs r
        (fun i : G =>
         path_forall (legs i) (r i) (path_legs i))) j)
  x =
ap (D _f f)
  (apD10
     (apD10
        (path_forall legs r
           (fun i : G =>
            path_forall (legs i) (r i) (path_legs i)))
        i) x) @ pp_r i j f x
    rewrite 3 eisretr.
H: Funext
X: Type
G: Graph
D: Diagram G
legs: forall i : G, X -> D i
pp_q: forall (i j : G) (g : G i j),
(fun x : X => (D _f g) (legs i x)) == legs j
r: forall i : G, X -> D i
pp_r: forall (i j : G) (g : G i j),
(fun x : X => (D _f g) (r i x)) == r j
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 : X),
legs_comm
  {|
    legs := legs; legs_comm := pp_q
  |} i j g x @ path_legs j x =
ap (D _f g) (path_legs i x) @
legs_comm
  {| legs := r; legs_comm := pp_r |}
  i j g x
i, j: G
f: G i j
x: X
pp_q i j f x @ path_legs j x =
ap (D _f f) (path_legs i x) @ pp_r i j f x
    apply path_legs_comm.
  Defined.

  (** ** Precomposition for cones *)

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

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

  (** ** Universality of a cone. *)

  (** A limit will be the extremity of an universal cone. *)

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

  Class UniversalCone (C : Cone X D) := {
    is_universal :: forall Y, IsEquiv (@cone_precompose C Y);
    }.
  Coercion is_universal : UniversalCone >-> Funclass.

End Cone.

(** We now prove several functoriality results, first on cone and then on limits. *)

Section FunctorialityCone.

  Context `{Funext} {G : Graph}.

  (** ** Precomposition for cones *)

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

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

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

  (** ** Postcomposition for cones *)

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

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

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

  Definition cone_postcompose_identity (D : Diagram G) (X : Type)
    : cone_postcompose (X:=X) (diagram_idmap D) == idmap.
H: Funext
G: Graph
D: Diagram G
X: Type
cone_postcompose (diagram_idmap D) == idmap
  Proof.
H: Funext
G: Graph
D: Diagram G
X: Type
cone_postcompose (diagram_idmap D) == idmap
    intro C; srapply path_cone; simpl.
H: Funext
G: Graph
D: Diagram G
X: Type
C: Cone X D
forall i : G, (fun x : X => C i x) == C i
H: Funext
G: Graph
D: Diagram G
X: Type
C: Cone X D
forall (i j : G) (g : G i j) (x : X),
(1 @ ap idmap (legs_comm C i j g x)) @ ?Goal j x =
ap (D _f g) (?Goal i x) @ legs_comm C i j g x
    1: reflexivity.
H: Funext
G: Graph
D: Diagram G
X: Type
C: Cone X D
forall (i j : G) (g : G i j) (x : X),
(1 @ ap idmap (legs_comm C i j g x)) @
(fun (i0 : G) (x0 : X) => 1) j x =
ap (D _f g) ((fun (i0 : G) (x0 : X) => 1) i x) @
legs_comm C i j g x
    intros; simpl.
H: Funext
G: Graph
D: Diagram G
X: Type
C: Cone X D
i, j: G
g: G i j
x: X
(1 @ ap idmap (legs_comm C i j g x)) @ 1 =
1 @ legs_comm C i j g x
    refine (_ @ (concat_1p _)^).
H: Funext
G: Graph
D: Diagram G
X: Type
C: Cone X D
i, j: G
g: G i j
x: X
(1 @ ap idmap (legs_comm C i j g x)) @ 1 =
legs_comm C i j g x
    exact (concat_p1 _ @ concat_1p _ @ ap_idmap _).
  Defined.

  Definition cone_postcompose_comp {D1 D2 D3 : Diagram G}
    (m2 : DiagramMap D2 D3) (m1 : DiagramMap D1 D2) (X : Type)
    : (cone_postcompose (X:=X) m2) o (cone_postcompose m1)
      == cone_postcompose (diagram_comp m2 m1).
H: Funext
G: Graph
D1, D2, D3: Diagram G
m2: DiagramMap D2 D3
m1: DiagramMap D1 D2
X: Type
cone_postcompose m2 o cone_postcompose m1 ==
cone_postcompose (diagram_comp m2 m1)
  Proof.
H: Funext
G: Graph
D1, D2, D3: Diagram G
m2: DiagramMap D2 D3
m1: DiagramMap D1 D2
X: Type
cone_postcompose m2 o cone_postcompose m1 ==
cone_postcompose (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: Cone X D1
cone_postcompose m2 (cone_postcompose m1 C) =
cone_postcompose (diagram_comp m2 m1) C
    srapply path_cone.
H: Funext
G: Graph
D1, D2, D3: Diagram G
m2: DiagramMap D2 D3
m1: DiagramMap D1 D2
X: Type
C: Cone X D1
forall i : G,
cone_postcompose m2 (cone_postcompose m1 C) i ==
cone_postcompose (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: Cone X D1
forall (i j : G) (g : G i j) (x : X),
legs_comm
  (cone_postcompose m2 (cone_postcompose m1 C)) i j g
  x @ ?path_legs j x =
ap (D3 _f g) (?path_legs i x) @
legs_comm (cone_postcompose (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: Cone X D1
forall (i j : G) (g : G i j) (x : X),
legs_comm
  (cone_postcompose m2 (cone_postcompose m1 C)) i j g
  x @ (fun (i0 : G) (x0 : X) => 1) j x =
ap (D3 _f g) ((fun (i0 : G) (x0 : X) => 1) i x) @
legs_comm (cone_postcompose (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: Cone X D1
i, j: G
g: G i j
x: X
(DiagramMap_comm m2 g (m1 i (C i x)) @
 ap (m2 j)
   (DiagramMap_comm m1 g (C i x) @
    ap (m1 j) (legs_comm C i j g x))) @ 1 =
1 @
(CommutativeSquares.comm_square_comp
   (DiagramMap_comm m1 g) (DiagramMap_comm m2 g)
   (C i x) @
 ap (fun x : D1 j => m2 j (m1 j x))
   (legs_comm C i j g 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: Cone X D1
i, j: G
g: G i j
x: X
DiagramMap_comm m2 g (m1 i (C i x)) @
ap (m2 j)
  (DiagramMap_comm m1 g (C i x) @
   ap (m1 j) (legs_comm C i j g x)) =
CommutativeSquares.comm_square_comp
  (DiagramMap_comm m1 g) (DiagramMap_comm m2 g)
  (C i x) @
ap (fun x : D1 j => m2 j (m1 j x))
  (legs_comm C i j g 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: Cone X D1
i, j: G
g: G i j
x: X
DiagramMap_comm m2 g (m1 i (C i x)) @
ap (m2 j)
  (DiagramMap_comm m1 g (C i x) @
   ap (m1 j) (legs_comm C i j g x)) =
(DiagramMap_comm m2 g (m1 i (C i x)) @
 ap (m2 j) (DiagramMap_comm m1 g (C i x))) @
ap (fun x : D1 j => m2 j (m1 j x))
  (legs_comm C i j g 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: Cone X D1
i, j: G
g: G i j
x: X
DiagramMap_comm m2 g (m1 i (C i x)) @
ap (m2 j)
  (DiagramMap_comm m1 g (C i x) @
   ap (m1 j) (legs_comm C i j g x)) =
DiagramMap_comm m2 g (m1 i (C i x)) @
(ap (m2 j) (DiagramMap_comm m1 g (C i x)) @
 ap (fun x : D1 j => m2 j (m1 j x))
   (legs_comm C i j g x))
    apply ap.
H: Funext
G: Graph
D1, D2, D3: Diagram G
m2: DiagramMap D2 D3
m1: DiagramMap D1 D2
X: Type
C: Cone X D1
i, j: G
g: G i j
x: X
ap (m2 j)
  (DiagramMap_comm m1 g (C i x) @
   ap (m1 j) (legs_comm C i j g x)) =
ap (m2 j) (DiagramMap_comm m1 g (C i x)) @
ap (fun x : D1 j => m2 j (m1 j x))
  (legs_comm C i j 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: Cone X D1
i, j: G
g: G i j
x: X
ap (m2 j) (DiagramMap_comm m1 g (C i x)) @
ap (m2 j) (ap (m1 j) (legs_comm C i j g x)) =
ap (m2 j) (DiagramMap_comm m1 g (C i x)) @
ap (fun x : D1 j => m2 j (m1 j x))
  (legs_comm C i j g x)
    apply ap.
H: Funext
G: Graph
D1, D2, D3: Diagram G
m2: DiagramMap D2 D3
m1: DiagramMap D1 D2
X: Type
C: Cone X D1
i, j: G
g: G i j
x: X
ap (m2 j) (ap (m1 j) (legs_comm C i j g x)) =
ap (fun x : D1 j => m2 j (m1 j x))
  (legs_comm C i j g x)
    symmetry.
H: Funext
G: Graph
D1, D2, D3: Diagram G
m2: DiagramMap D2 D3
m1: DiagramMap D1 D2
X: Type
C: Cone X D1
i, j: G
g: G i j
x: X
ap (fun x : D1 j => m2 j (m1 j x))
  (legs_comm C i j g x) =
ap (m2 j) (ap (m1 j) (legs_comm C i j g x))
    by apply ap_compose.
  Defined.

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

  Definition cone_postcompose_precompose {D1 D2 : Diagram G}
             (m : DiagramMap D1 D2) `(f : Y -> X) (C : Cone X D1)
    : cone_precompose (cone_postcompose m C) f
      = cone_postcompose m (cone_precompose C f).
H: Funext
G: Graph
D1, D2: Diagram G
m: DiagramMap D1 D2
Y, X: Type
f: Y -> X
C: Cone X D1
cone_precompose (cone_postcompose m C) f =
cone_postcompose m (cone_precompose C f)
  Proof.
H: Funext
G: Graph
D1, D2: Diagram G
m: DiagramMap D1 D2
Y, X: Type
f: Y -> X
C: Cone X D1
cone_precompose (cone_postcompose m C) f =
cone_postcompose m (cone_precompose C f)
    srapply path_cone; intro i.
H: Funext
G: Graph
D1, D2: Diagram G
m: DiagramMap D1 D2
Y, X: Type
f: Y -> X
C: Cone X D1
i: G
cone_precompose (cone_postcompose m C) f i ==
cone_postcompose m (cone_precompose C f) i
H: Funext
G: Graph
D1, D2: Diagram G
m: DiagramMap D1 D2
Y, X: Type
f: Y -> X
C: Cone X D1
i: G
forall (j : G) (g : G i j) (x : Y),
legs_comm (cone_precompose (cone_postcompose m C) f) i
  j g x @ (fun i : G => ?Goal) j x =
ap (D2 _f g) ((fun i : G => ?Goal) i x) @
legs_comm (cone_postcompose m (cone_precompose C f)) i
  j g x
    1: reflexivity.
H: Funext
G: Graph
D1, D2: Diagram G
m: DiagramMap D1 D2
Y, X: Type
f: Y -> X
C: Cone X D1
i: G
forall (j : G) (g : G i j) (x : Y),
legs_comm (cone_precompose (cone_postcompose m C) f) i
  j g x @ (fun (i : G) (x0 : Y) => 1) j x =
ap (D2 _f g) ((fun (i : G) (x0 : Y) => 1) i x) @
legs_comm (cone_postcompose m (cone_precompose C f)) i
  j g x
    intros j g x; simpl.
H: Funext
G: Graph
D1, D2: Diagram G
m: DiagramMap D1 D2
Y, X: Type
f: Y -> X
C: Cone X D1
i, j: G
g: G i j
x: Y
(DiagramMap_comm m g (C i (f x)) @
 ap (m j) (legs_comm C i j g (f x))) @ 1 =
1 @
(DiagramMap_comm m g (C i (f x)) @
 ap (m j) (legs_comm C i j g (f x)))
    apply concat_p1_1p.
  Defined.

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

  #[export] Instance cone_precompose_equiv {D1 D2 : Diagram G}
    (m : D1 ~d~ D2) (X : Type) : IsEquiv (cone_postcompose (X:=X) m).
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
X: Type
IsEquiv (cone_postcompose m)
  Proof.
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
X: Type
IsEquiv (cone_postcompose m)
    srapply isequiv_adjointify.
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
X: Type
Cone X D2 -> Cone X D1
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
X: Type
cone_postcompose m o ?g == idmap
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
X: Type
?g o cone_postcompose m == idmap
    1: exact (cone_postcompose (diagram_equiv_inv m)).
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
X: Type
cone_postcompose m
o cone_postcompose (diagram_equiv_inv m) == idmap
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
X: Type
cone_postcompose (diagram_equiv_inv m)
o cone_postcompose m == idmap
    +
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
X: Type
cone_postcompose m
o cone_postcompose (diagram_equiv_inv m) == idmap intros C.
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
X: Type
C: Cone X D2
cone_postcompose m
  (cone_postcompose (diagram_equiv_inv m) C) = C
      etransitivity.
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
X: Type
C: Cone X D2
cone_postcompose m
  (cone_postcompose (diagram_equiv_inv m) C) = ?Goal
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
X: Type
C: Cone X D2
?Goal = C
      -
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
X: Type
C: Cone X D2
cone_postcompose m
  (cone_postcompose (diagram_equiv_inv m) C) = ?Goal apply cone_postcompose_comp.
      -
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
X: Type
C: Cone X D2
cone_postcompose
  (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: Cone X D2
cone_postcompose (diagram_idmap D2) C = C
        apply cone_postcompose_identity.
    +
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
X: Type
cone_postcompose (diagram_equiv_inv m)
o cone_postcompose m == idmap intros C.
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
X: Type
C: Cone X D1
cone_postcompose (diagram_equiv_inv m)
  (cone_postcompose m C) = C
      etransitivity.
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
X: Type
C: Cone X D1
cone_postcompose (diagram_equiv_inv m)
  (cone_postcompose m C) = ?Goal
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
X: Type
C: Cone X D1
?Goal = C
      -
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
X: Type
C: Cone X D1
cone_postcompose (diagram_equiv_inv m)
  (cone_postcompose m C) = ?Goal apply cone_postcompose_comp.
      -
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
X: Type
C: Cone X D1
cone_postcompose
  (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: Cone X D1
cone_postcompose (diagram_idmap D1) C = C
        apply cone_postcompose_identity.
  Defined.

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

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

  (** ** Universality preservation *)

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

  #[export] Instance cone_postcompose_equiv_universality {D1 D2 : Diagram G}
    (m: D1 ~d~ D2) {X} (C : Cone X D1) (_ : UniversalCone C)
    : UniversalCone (cone_postcompose (X:=X) m C).
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
X: Type
C: Cone X D1
X0: UniversalCone C
UniversalCone (cone_postcompose m C)
  Proof.
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
X: Type
C: Cone X D1
X0: UniversalCone C
UniversalCone (cone_postcompose m C)
    srapply Build_UniversalCone; intro.
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
X: Type
C: Cone X D1
X0: UniversalCone C
Y: Type
IsEquiv (cone_precompose (cone_postcompose m C))
    rewrite (path_forall _ _ (fun f => cone_postcompose_precompose m f C)).
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
X: Type
C: Cone X D1
X0: UniversalCone C
Y: Type
IsEquiv
  (fun f : Y -> X =>
   cone_postcompose m (cone_precompose C f))
    rapply isequiv_compose.
  Defined.

  #[export] Instance cone_precompose_equiv_universality {D: Diagram G} `(f: Y <~> X)
    (C : Cone X D) (_ : UniversalCone C)
    : UniversalCone (cone_precompose C f).
H: Funext
G: Graph
D: Diagram G
Y, X: Type
f: Y <~> X
C: Cone X D
X0: UniversalCone C
UniversalCone (cone_precompose C f)
  Proof.
H: Funext
G: Graph
D: Diagram G
Y, X: Type
f: Y <~> X
C: Cone X D
X0: UniversalCone C
UniversalCone (cone_precompose C f)
    srapply Build_UniversalCone; intro.
H: Funext
G: Graph
D: Diagram G
Y, X: Type
f: Y <~> X
C: Cone X D
X0: UniversalCone C
Y0: Type
IsEquiv (cone_precompose (cone_precompose C f))
    rewrite <- (path_forall _ _ (fun g => cone_precompose_comp g f C)).
H: Funext
G: Graph
D: Diagram G
Y, X: Type
f: Y <~> X
C: Cone X D
X0: UniversalCone C
Y0: Type
IsEquiv
  (fun g : Y0 -> Y =>
   cone_precompose C (fun x : Y0 => f (g x)))
    rapply isequiv_compose.
  Defined.

End FunctorialityCone.