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

Local Open Scope path_scope.

(** This file contains the definition of diagrams, diagram maps and equivalences of diagrams. *)

(** * Diagrams *)

(** A [Diagram] over a graph [G] associates a type to each point of the graph and a function to each arrow. *)

Record Diagram (G : Graph) := {
  obj : G -> Type;
  arr {i j : G} : G i j -> obj i -> obj j
}.

Arguments obj [G] D i : rename.
Arguments arr [G] D [i j] g x : rename.

Coercion obj : Diagram >-> Funclass.
Notation "D '_f' g" := (arr D g).

Section Diagram.
  Context `{Funext} {G: Graph}.

  (** [path_diagram] says when two diagrams are equals (up to funext). *)

  Definition path_diagram_naive (D1 D2 : Diagram G)
    (P := fun D' => forall i j, G i j -> (D' i -> D' j))
    (path_obj : obj D1 = obj D2)
    (path_arr : transport P path_obj (arr D1) = arr D2)
    : D1 = D2 :=
    match path_arr in (_ = v1)
      return D1 = {|obj := obj D2; arr := v1 |}
    with
      | idpath => match path_obj in (_ = v0)
        return D1 = {|obj := v0; arr := path_obj # (arr D1) |}
      with
        | idpath => 1
      end
    end.

  Definition path_diagram (D1 D2 : Diagram G)
    (path_obj : forall i, D1 i = D2 i)
    (path_arr : forall i j (g : G i j) x,
      transport idmap (path_obj j) (D1 _f g x)
      = D2 _f g (transport idmap (path_obj i) x))
    : D1 = D2.
H: Funext
G: Graph
D1, D2: Diagram G
path_obj: forall i : G, D1 i = D2 i
path_arr: forall (i j : G) (g : G i j) 
(x : D1 i),
transport idmap (path_obj j) ((D1 _f g) x) =
(D2 _f g) (transport idmap (path_obj i) x)
D1 = D2
  Proof.
H: Funext
G: Graph
D1, D2: Diagram G
path_obj: forall i : G, D1 i = D2 i
path_arr: forall (i j : G) (g : G i j) 
(x : D1 i),
transport idmap (path_obj j) ((D1 _f g) x) =
(D2 _f g) (transport idmap (path_obj i) x)
D1 = D2
    srapply path_diagram_naive; funext i.
H: Funext
G: Graph
D1, D2: Diagram G
path_obj: forall i : G, D1 i = D2 i
path_arr: forall (i j : G) (g : G i j) 
(x : D1 i),
transport idmap (path_obj j) ((D1 _f g) x) =
(D2 _f g) (transport idmap (path_obj i) x)
i: G
D1 i = D2 i
H: Funext
G: Graph
D1, D2: Diagram G
path_obj: forall i : G, D1 i = D2 i
path_arr: forall (i j : G) (g : G i j) 
(x : D1 i),
transport idmap (path_obj j) ((D1 _f g) x) =
(D2 _f g) (transport idmap (path_obj i) x)
i: G
transport
  (fun D' : G -> Type =>
   forall i j : G, G i j -> D' i -> D' j)
  (path_forall D1 D2 (fun i : G => ?Goal)) 
  (arr D1) i = arr D2 (i:=i)
    1: apply path_obj.
H: Funext
G: Graph
D1, D2: Diagram G
path_obj: forall i : G, D1 i = D2 i
path_arr: forall (i j : G) (g : G i j) 
(x : D1 i),
transport idmap (path_obj j) ((D1 _f g) x) =
(D2 _f g) (transport idmap (path_obj i) x)
i: G
transport
  (fun D' : G -> Type =>
   forall i j : G, G i j -> D' i -> D' j)
  (path_forall D1 D2 (fun i : G => path_obj i))
  (arr D1) i = arr D2 (i:=i)
    funext j g x.
H: Funext
G: Graph
D1, D2: Diagram G
path_obj: forall i : G, D1 i = D2 i
path_arr: forall (i j : G) (g : G i j) 
(x : D1 i),
transport idmap (path_obj j) ((D1 _f g) x) =
(D2 _f g) (transport idmap (path_obj i) x)
i, j: G
g: G i j
x: D2 i
transport
  (fun D' : G -> Type =>
   forall i j : G, G i j -> D' i -> D' j)
  (path_forall D1 D2 (fun i : G => path_obj i))
  (arr D1) i j g x = (D2 _f g) x
    rewrite 3 transport_forall_constant, transport_arrow.
H: Funext
G: Graph
D1, D2: Diagram G
path_obj: forall i : G, D1 i = D2 i
path_arr: forall (i j : G) (g : G i j) 
(x : D1 i),
transport idmap (path_obj j) ((D1 _f g) x) =
(D2 _f g) (transport idmap (path_obj i) x)
i, j: G
g: G i j
x: D2 i
transport (fun x : G -> Type => x j)
  (path_forall D1 D2 (fun i : G => path_obj i))
  ((D1 _f g)
     (transport (fun x : G -> Type => x i)
        (path_forall D1 D2 (fun i : G => path_obj i))^
        x)) = (D2 _f g) x
    transport_path_forall_hammer.
H: Funext
G: Graph
D1, D2: Diagram G
path_obj: forall i : G, D1 i = D2 i
path_arr: forall (i j : G) (g : G i j) 
(x : D1 i),
transport idmap (path_obj j) ((D1 _f g) x) =
(D2 _f g) (transport idmap (path_obj i) x)
i, j: G
g: G i j
x: D2 i
transport idmap (path_obj j)
  ((D1 _f g)
     (transport (fun x : G -> Type => x i)
        (path_forall D1 D2 (fun i : G => path_obj i))^
        x)) = (D2 _f g) x
    refine (_ @ path_arr i j g (transport idmap (path_obj i)^ x) @ _).
H: Funext
G: Graph
D1, D2: Diagram G
path_obj: forall i : G, D1 i = D2 i
path_arr: forall (i j : G) (g : G i j) 
(x : D1 i),
transport idmap (path_obj j) ((D1 _f g) x) =
(D2 _f g) (transport idmap (path_obj i) x)
i, j: G
g: G i j
x: D2 i
transport idmap (path_obj j)
  ((D1 _f g)
     (transport (fun x : G -> Type => x i)
        (path_forall D1 D2 (fun i : G => path_obj i))^
        x)) =
transport idmap (path_obj j)
  ((D1 _f g) (transport idmap (path_obj i)^ x))
H: Funext
G: Graph
D1, D2: Diagram G
path_obj: forall i : G, D1 i = D2 i
path_arr: forall (i j : G) (g : G i j) 
(x : D1 i),
transport idmap (path_obj j) ((D1 _f g) x) =
(D2 _f g) (transport idmap (path_obj i) x)
i, j: G
g: G i j
x: D2 i
(D2 _f g)
  (transport idmap (path_obj i)
     (transport idmap (path_obj i)^ x)) = 
(D2 _f g) x
    {
H: Funext
G: Graph
D1, D2: Diagram G
path_obj: forall i : G, D1 i = D2 i
path_arr: forall (i j : G) (g : G i j) 
(x : D1 i),
transport idmap (path_obj j) ((D1 _f g) x) =
(D2 _f g) (transport idmap (path_obj i) x)
i, j: G
g: G i j
x: D2 i
transport idmap (path_obj j)
  ((D1 _f g)
     (transport (fun x : G -> Type => x i)
        (path_forall D1 D2 (fun i : G => path_obj i))^
        x)) =
transport idmap (path_obj j)
  ((D1 _f g) (transport idmap (path_obj i)^ x)) do 3 f_ap.
H: Funext
G: Graph
D1, D2: Diagram G
path_obj: forall i : G, D1 i = D2 i
path_arr: forall (i j : G) (g : G i j) 
(x : D1 i),
transport idmap (path_obj j) ((D1 _f g) x) =
(D2 _f g) (transport idmap (path_obj i) x)
i, j: G
g: G i j
x: D2 i
transport (fun x : G -> Type => x i)
  (path_forall D1 D2 (fun i : G => path_obj i))^ =
transport idmap (path_obj i)^
      rewrite <- path_forall_V.
H: Funext
G: Graph
D1, D2: Diagram G
path_obj: forall i : G, D1 i = D2 i
path_arr: forall (i j : G) (g : G i j) 
(x : D1 i),
transport idmap (path_obj j) ((D1 _f g) x) =
(D2 _f g) (transport idmap (path_obj i) x)
i, j: G
g: G i j
x: D2 i
transport (fun x : G -> Type => x i)
  (path_forall D2 D1 (fun x : G => (path_obj x)^)) =
transport idmap (path_obj i)^
      funext y.
H: Funext
G: Graph
D1, D2: Diagram G
path_obj: forall i : G, D1 i = D2 i
path_arr: forall (i j : G) (g : G i j) 
(x : D1 i),
transport idmap (path_obj j) ((D1 _f g) x) =
(D2 _f g) (transport idmap (path_obj i) x)
i, j: G
g: G i j
x, y: D2 i
transport (fun x : G -> Type => x i)
  (path_forall D2 D1 (fun x : G => (path_obj x)^)) y =
transport idmap (path_obj i)^ y
      by transport_path_forall_hammer. }
H: Funext
G: Graph
D1, D2: Diagram G
path_obj: forall i : G, D1 i = D2 i
path_arr: forall (i j : G) (g : G i j) 
(x : D1 i),
transport idmap (path_obj j) ((D1 _f g) x) =
(D2 _f g) (transport idmap (path_obj i) x)
i, j: G
g: G i j
x: D2 i
(D2 _f g)
  (transport idmap (path_obj i)
     (transport idmap (path_obj i)^ x)) = (D2 _f g) x
    f_ap.
H: Funext
G: Graph
D1, D2: Diagram G
path_obj: forall i : G, D1 i = D2 i
path_arr: forall (i j : G) (g : G i j) 
(x : D1 i),
transport idmap (path_obj j) ((D1 _f g) x) =
(D2 _f g) (transport idmap (path_obj i) x)
i, j: G
g: G i j
x: D2 i
transport idmap (path_obj i)
  (transport idmap (path_obj i)^ x) = x
    exact (transport_pV idmap _ x).
  Defined.

  (** * Diagram map *)

  (** A map between two diagrams is a family of maps between the types of the diagrams making commuting the squares formed with the arrows. *)

  Record DiagramMap (D1 D2 : Diagram G) := {
    DiagramMap_obj  :> forall i, D1 i -> D2 i;
    DiagramMap_comm :  forall i j (g: G i j) x,
          D2 _f g (DiagramMap_obj i x) = DiagramMap_obj j (D1 _f g x)
  }.

  Global Arguments DiagramMap_obj [D1 D2] m i x : rename.
  Global Arguments DiagramMap_comm  [D1 D2] m [i j] f x : rename.
  Global Arguments Build_DiagramMap [D1 D2] _ _.

  (** [path_DiagramMap] says when two maps are equals (up to funext). *)

  Definition path_DiagramMap {D1 D2 : Diagram G}
    {m1 m2 : DiagramMap D1 D2} (h_obj : forall i, m1 i == m2 i)
    (h_comm : forall i j (g : G i j) x,
      DiagramMap_comm m1 g x @ h_obj j (D1 _f g x)
      = ap (D2 _f g) (h_obj i x) @ DiagramMap_comm m2 g x)
    : m1 = m2.
H: Funext
G: Graph
D1, D2: Diagram G
m1, m2: DiagramMap D1 D2
h_obj: forall i : G, m1 i == m2 i
h_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
DiagramMap_comm m1 g x @
h_obj j ((D1 _f g) x) =
ap (D2 _f g) (h_obj i x) @
DiagramMap_comm m2 g x
m1 = m2
  Proof.
H: Funext
G: Graph
D1, D2: Diagram G
m1, m2: DiagramMap D1 D2
h_obj: forall i : G, m1 i == m2 i
h_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
DiagramMap_comm m1 g x @
h_obj j ((D1 _f g) x) =
ap (D2 _f g) (h_obj i x) @
DiagramMap_comm m2 g x
m1 = m2
    destruct m1 as [m1_obj m1_comm].
H: Funext
G: Graph
D1, D2: Diagram G
m1_obj: forall i : G, D1 i -> D2 i
m1_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
(D2 _f g) (m1_obj i x) =
m1_obj j ((D1 _f g) x)
m2: DiagramMap D1 D2
h_obj: forall i : G,
{|
  DiagramMap_obj := m1_obj;
  DiagramMap_comm := m1_comm
|} i == m2 i
h_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
DiagramMap_comm
  {|
    DiagramMap_obj := m1_obj;
    DiagramMap_comm := m1_comm
  |} g x @ h_obj j ((D1 _f g) x) =
ap (D2 _f g) (h_obj i x) @
DiagramMap_comm m2 g x
{|
  DiagramMap_obj := m1_obj; DiagramMap_comm := m1_comm
|} = m2
    destruct m2 as [m2_obj m2_comm].
H: Funext
G: Graph
D1, D2: Diagram G
m1_obj: forall i : G, D1 i -> D2 i
m1_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
(D2 _f g) (m1_obj i x) =
m1_obj j ((D1 _f g) x)
m2_obj: forall i : G, D1 i -> D2 i
m2_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
(D2 _f g) (m2_obj i x) =
m2_obj j ((D1 _f g) x)
h_obj: forall i : G,
{|
  DiagramMap_obj := m1_obj;
  DiagramMap_comm := m1_comm
|} i ==
{|
  DiagramMap_obj := m2_obj;
  DiagramMap_comm := m2_comm
|} i
h_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
DiagramMap_comm
  {|
    DiagramMap_obj := m1_obj;
    DiagramMap_comm := m1_comm
  |} g x @ h_obj j ((D1 _f g) x) =
ap (D2 _f g) (h_obj i x) @
DiagramMap_comm
  {|
    DiagramMap_obj := m2_obj;
    DiagramMap_comm := m2_comm
  |} g x
{|
  DiagramMap_obj := m1_obj; DiagramMap_comm := m1_comm
|} =
{|
  DiagramMap_obj := m2_obj; DiagramMap_comm := m2_comm
|}
    simpl in *.
H: Funext
G: Graph
D1, D2: Diagram G
m1_obj: forall i : G, D1 i -> D2 i
m1_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
(D2 _f g) (m1_obj i x) =
m1_obj j ((D1 _f g) x)
m2_obj: forall i : G, D1 i -> D2 i
m2_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
(D2 _f g) (m2_obj i x) =
m2_obj j ((D1 _f g) x)
h_obj: forall i : G, m1_obj i == m2_obj i
h_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
m1_comm i j g x @ h_obj j ((D1 _f g) x) =
ap (D2 _f g) (h_obj i x) @ m2_comm i j g x
{|
  DiagramMap_obj := m1_obj; DiagramMap_comm := m1_comm
|} =
{|
  DiagramMap_obj := m2_obj; DiagramMap_comm := m2_comm
|}
    revert h_obj h_comm.
H: Funext
G: Graph
D1, D2: Diagram G
m1_obj: forall i : G, D1 i -> D2 i
m1_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
(D2 _f g) (m1_obj i x) =
m1_obj j ((D1 _f g) x)
m2_obj: forall i : G, D1 i -> D2 i
m2_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
(D2 _f g) (m2_obj i x) =
m2_obj j ((D1 _f g) x)
forall h_obj : forall i : G, m1_obj i == m2_obj i,
(forall (i j : G) (g : G i j) (x : D1 i),
 m1_comm i j g x @ h_obj j ((D1 _f g) x) =
 ap (D2 _f g) (h_obj i x) @ m2_comm i j g x) ->
{|
  DiagramMap_obj := m1_obj; DiagramMap_comm := m1_comm
|} =
{|
  DiagramMap_obj := m2_obj; DiagramMap_comm := m2_comm
|}
    set (E := (@equiv_functor_forall _
       G (fun i => m1_obj i = m2_obj i)
       G (fun i => m1_obj i == m2_obj i)
       idmap _
       (fun i => @apD10 _ _ (m1_obj i) (m2_obj i)))
       (fun i => isequiv_apD10 _ _ _ _)).
H: Funext
G: Graph
D1, D2: Diagram G
m1_obj: forall i : G, D1 i -> D2 i
m1_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
(D2 _f g) (m1_obj i x) =
m1_obj j ((D1 _f g) x)
m2_obj: forall i : G, D1 i -> D2 i
m2_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
(D2 _f g) (m2_obj i x) =
m2_obj j ((D1 _f g) x)
E:= equiv_functor_forall idmap (fun i : G => apD10): (forall a : G,
 (fun i : G => m1_obj i = m2_obj i) a) <~>
(forall b : G,
 (fun i : G => m1_obj i == m2_obj i) b)
forall h_obj : forall i : G, m1_obj i == m2_obj i,
(forall (i j : G) (g : G i j) (x : D1 i),
 m1_comm i j g x @ h_obj j ((D1 _f g) x) =
 ap (D2 _f g) (h_obj i x) @ m2_comm i j g x) ->
{|
  DiagramMap_obj := m1_obj; DiagramMap_comm := m1_comm
|} =
{|
  DiagramMap_obj := m2_obj; DiagramMap_comm := m2_comm
|}
    equiv_intro E h_obj.
H: Funext
G: Graph
D1, D2: Diagram G
m1_obj: forall i : G, D1 i -> D2 i
m1_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
(D2 _f g) (m1_obj i x) =
m1_obj j ((D1 _f g) x)
m2_obj: forall i : G, D1 i -> D2 i
m2_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
(D2 _f g) (m2_obj i x) =
m2_obj j ((D1 _f g) x)
E:= equiv_functor_forall idmap (fun i : G => apD10): (forall a : G,
 (fun i : G => m1_obj i = m2_obj i) a) <~>
(forall b : G,
 (fun i : G => m1_obj i == m2_obj i) b)
h_obj: forall a : G, m1_obj a = m2_obj a
(forall (i j : G) (g : G i j) (x : D1 i),
 m1_comm i j g x @ E h_obj j ((D1 _f g) x) =
 ap (D2 _f g) (E h_obj i x) @ m2_comm i j g x) ->
{|
  DiagramMap_obj := m1_obj; DiagramMap_comm := m1_comm
|} =
{|
  DiagramMap_obj := m2_obj; DiagramMap_comm := m2_comm
|}
    revert h_obj.
H: Funext
G: Graph
D1, D2: Diagram G
m1_obj: forall i : G, D1 i -> D2 i
m1_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
(D2 _f g) (m1_obj i x) =
m1_obj j ((D1 _f g) x)
m2_obj: forall i : G, D1 i -> D2 i
m2_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
(D2 _f g) (m2_obj i x) =
m2_obj j ((D1 _f g) x)
E:= equiv_functor_forall idmap (fun i : G => apD10): (forall a : G,
 (fun i : G => m1_obj i = m2_obj i) a) <~>
(forall b : G,
 (fun i : G => m1_obj i == m2_obj i) b)
forall h_obj : forall a : G, m1_obj a = m2_obj a,
(forall (i j : G) (g : G i j) (x : D1 i),
 m1_comm i j g x @ E h_obj j ((D1 _f g) x) =
 ap (D2 _f g) (E h_obj i x) @ m2_comm i j g x) ->
{|
  DiagramMap_obj := m1_obj; DiagramMap_comm := m1_comm
|} =
{|
  DiagramMap_obj := m2_obj; DiagramMap_comm := m2_comm
|}
    equiv_intro (@apD10 _ _ m1_obj m2_obj) h_obj.
H: Funext
G: Graph
D1, D2: Diagram G
m1_obj: forall i : G, D1 i -> D2 i
m1_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
(D2 _f g) (m1_obj i x) =
m1_obj j ((D1 _f g) x)
m2_obj: forall i : G, D1 i -> D2 i
m2_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
(D2 _f g) (m2_obj i x) =
m2_obj j ((D1 _f g) x)
E:= equiv_functor_forall idmap (fun i : G => apD10): (forall a : G,
 (fun i : G => m1_obj i = m2_obj i) a) <~>
(forall b : G,
 (fun i : G => m1_obj i == m2_obj i) b)
h_obj: m1_obj = m2_obj
(forall (i j : G) (g : G i j) (x : D1 i),
 m1_comm i j g x @ E (apD10 h_obj) j ((D1 _f g) x) =
 ap (D2 _f g) (E (apD10 h_obj) i x) @ m2_comm i j g x) ->
{|
  DiagramMap_obj := m1_obj; DiagramMap_comm := m1_comm
|} =
{|
  DiagramMap_obj := m2_obj; DiagramMap_comm := m2_comm
|}
    destruct h_obj; simpl.
H: Funext
G: Graph
D1, D2: Diagram G
m1_obj: forall i : G, D1 i -> D2 i
m1_comm, m2_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
(D2 _f g) (m1_obj i x) =
m1_obj j ((D1 _f g) x)
E:= equiv_functor_forall idmap (fun i : G => apD10): (forall a : G, m1_obj a = m1_obj a) <~>
(forall b : G, m1_obj b == m1_obj b)
(forall (i j : G) (g : G i j) (x : D1 i),
 m1_comm i j g x @
 functor_forall idmap (fun i0 : G => apD10) (apD10 1)
   j ((D1 _f g) x) = 1 @ m2_comm i j g x) ->
{|
  DiagramMap_obj := m1_obj; DiagramMap_comm := m1_comm
|} =
{|
  DiagramMap_obj := m1_obj; DiagramMap_comm := m2_comm
|}
    intros h_comm.
H: Funext
G: Graph
D1, D2: Diagram G
m1_obj: forall i : G, D1 i -> D2 i
m1_comm, m2_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
(D2 _f g) (m1_obj i x) =
m1_obj j ((D1 _f g) x)
E:= equiv_functor_forall idmap (fun i : G => apD10): (forall a : G, m1_obj a = m1_obj a) <~>
(forall b : G, m1_obj b == m1_obj b)
h_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
m1_comm i j g x @
functor_forall idmap (fun i0 : G => apD10)
  (apD10 1) j ((D1 _f g) x) =
1 @ m2_comm i j g x
{|
  DiagramMap_obj := m1_obj; DiagramMap_comm := m1_comm
|} =
{|
  DiagramMap_obj := m1_obj; DiagramMap_comm := m2_comm
|}
    assert (HH : m1_comm = m2_comm).
H: Funext
G: Graph
D1, D2: Diagram G
m1_obj: forall i : G, D1 i -> D2 i
m1_comm, m2_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
(D2 _f g) (m1_obj i x) =
m1_obj j ((D1 _f g) x)
E:= equiv_functor_forall idmap (fun i : G => apD10): (forall a : G, m1_obj a = m1_obj a) <~>
(forall b : G, m1_obj b == m1_obj b)
h_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
m1_comm i j g x @
functor_forall idmap (fun i0 : G => apD10)
  (apD10 1) j ((D1 _f g) x) =
1 @ m2_comm i j g x
m1_comm = m2_comm
H: Funext
G: Graph
D1, D2: Diagram G
m1_obj: forall i : G, D1 i -> D2 i
m1_comm, m2_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
(D2 _f g) (m1_obj i x) =
m1_obj j ((D1 _f g) x)
E:= equiv_functor_forall idmap (fun i : G => apD10): (forall a : G, m1_obj a = m1_obj a) <~>
(forall b : G, m1_obj b == m1_obj b)
h_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
m1_comm i j g x @
functor_forall idmap (fun i0 : G => apD10)
  (apD10 1) j ((D1 _f g) x) =
1 @ m2_comm i j g x
HH: m1_comm = m2_comm
{|
  DiagramMap_obj := m1_obj; DiagramMap_comm := m1_comm
|} =
{|
  DiagramMap_obj := m1_obj; DiagramMap_comm := m2_comm
|}
    {
H: Funext
G: Graph
D1, D2: Diagram G
m1_obj: forall i : G, D1 i -> D2 i
m1_comm, m2_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
(D2 _f g) (m1_obj i x) =
m1_obj j ((D1 _f g) x)
E:= equiv_functor_forall idmap (fun i : G => apD10): (forall a : G, m1_obj a = m1_obj a) <~>
(forall b : G, m1_obj b == m1_obj b)
h_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
m1_comm i j g x @
functor_forall idmap (fun i0 : G => apD10)
  (apD10 1) j ((D1 _f g) x) =
1 @ m2_comm i j g x
m1_comm = m2_comm funext i j f x.
H: Funext
G: Graph
D1, D2: Diagram G
m1_obj: forall i : G, D1 i -> D2 i
m1_comm, m2_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
(D2 _f g) (m1_obj i x) =
m1_obj j ((D1 _f g) x)
E:= equiv_functor_forall idmap (fun i : G => apD10): (forall a : G, m1_obj a = m1_obj a) <~>
(forall b : G, m1_obj b == m1_obj b)
h_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
m1_comm i j g x @
functor_forall idmap (fun i0 : G => apD10)
  (apD10 1) j ((D1 _f g) x) =
1 @ m2_comm i j g x
i, j: G
f: G i j
x: D1 i
m1_comm i j f x = m2_comm i j f x
      apply (concatR (concat_1p _)).
H: Funext
G: Graph
D1, D2: Diagram G
m1_obj: forall i : G, D1 i -> D2 i
m1_comm, m2_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
(D2 _f g) (m1_obj i x) =
m1_obj j ((D1 _f g) x)
E:= equiv_functor_forall idmap (fun i : G => apD10): (forall a : G, m1_obj a = m1_obj a) <~>
(forall b : G, m1_obj b == m1_obj b)
h_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
m1_comm i j g x @
functor_forall idmap (fun i0 : G => apD10)
  (apD10 1) j ((D1 _f g) x) =
1 @ m2_comm i j g x
i, j: G
f: G i j
x: D1 i
m1_comm i j f x = 1 @ m2_comm i j f x
      apply (concatR (h_comm _ _ _ _)).
H: Funext
G: Graph
D1, D2: Diagram G
m1_obj: forall i : G, D1 i -> D2 i
m1_comm, m2_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
(D2 _f g) (m1_obj i x) =
m1_obj j ((D1 _f g) x)
E:= equiv_functor_forall idmap (fun i : G => apD10): (forall a : G, m1_obj a = m1_obj a) <~>
(forall b : G, m1_obj b == m1_obj b)
h_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
m1_comm i j g x @
functor_forall idmap (fun i0 : G => apD10)
  (apD10 1) j ((D1 _f g) x) =
1 @ m2_comm i j g x
i, j: G
f: G i j
x: D1 i
m1_comm i j f x =
m1_comm i j f x @
functor_forall idmap (fun i : G => apD10) (apD10 1) j
  ((D1 _f f) x)
      apply inverse, concat_p1. }
H: Funext
G: Graph
D1, D2: Diagram G
m1_obj: forall i : G, D1 i -> D2 i
m1_comm, m2_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
(D2 _f g) (m1_obj i x) =
m1_obj j ((D1 _f g) x)
E:= equiv_functor_forall idmap (fun i : G => apD10): (forall a : G, m1_obj a = m1_obj a) <~>
(forall b : G, m1_obj b == m1_obj b)
h_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
m1_comm i j g x @
functor_forall idmap (fun i0 : G => apD10)
  (apD10 1) j ((D1 _f g) x) =
1 @ m2_comm i j g x
HH: m1_comm = m2_comm
{|
  DiagramMap_obj := m1_obj; DiagramMap_comm := m1_comm
|} =
{|
  DiagramMap_obj := m1_obj; DiagramMap_comm := m2_comm
|}
    destruct HH.
H: Funext
G: Graph
D1, D2: Diagram G
m1_obj: forall i : G, D1 i -> D2 i
m1_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
(D2 _f g) (m1_obj i x) =
m1_obj j ((D1 _f g) x)
E:= equiv_functor_forall idmap (fun i : G => apD10): (forall a : G, m1_obj a = m1_obj a) <~>
(forall b : G, m1_obj b == m1_obj b)
h_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
m1_comm i j g x @
functor_forall idmap (fun i0 : G => apD10)
  (apD10 1) j ((D1 _f g) x) =
1 @ m1_comm i j g x
{|
  DiagramMap_obj := m1_obj; DiagramMap_comm := m1_comm
|} =
{|
  DiagramMap_obj := m1_obj; DiagramMap_comm := m1_comm
|}
    reflexivity.
  Defined.

  (** ** Identity and composition for diagram maps. *)

  Definition diagram_idmap (D : Diagram G) : DiagramMap D D
    := Build_DiagramMap (fun _ => idmap) (fun _ _ _ _ => 1).

  Definition diagram_comp {D1 D2 D3 : Diagram G} (m2 : DiagramMap D2 D3)
             (m1 : DiagramMap D1 D2) : DiagramMap D1 D3.
H: Funext
G: Graph
D1, D2, D3: Diagram G
m2: DiagramMap D2 D3
m1: DiagramMap D1 D2
DiagramMap D1 D3
  Proof.
H: Funext
G: Graph
D1, D2, D3: Diagram G
m2: DiagramMap D2 D3
m1: DiagramMap D1 D2
DiagramMap D1 D3
    apply (Build_DiagramMap (fun i => m2 i o m1 i)).
H: Funext
G: Graph
D1, D2, D3: Diagram G
m2: DiagramMap D2 D3
m1: DiagramMap D1 D2
forall (i j : G) (g : G i j) (x : D1 i),
(D3 _f g) (m2 i (m1 i x)) = m2 j (m1 j ((D1 _f g) x))
    intros i j f.
H: Funext
G: Graph
D1, D2, D3: Diagram G
m2: DiagramMap D2 D3
m1: DiagramMap D1 D2
i, j: G
f: G i j
forall x : D1 i,
(D3 _f f) (m2 i (m1 i x)) = m2 j (m1 j ((D1 _f f) x))
    exact (comm_square_comp (DiagramMap_comm m1 f) (DiagramMap_comm m2 f)).
  Defined.

  (** * Diagram equivalences *)

  (** An equivalence of diagram is a diagram map whose functions are equivalences. *)

  Record diagram_equiv (D1 D2: Diagram G) :=
    { diag_equiv_map :> DiagramMap D1 D2;
      diag_equiv_isequiv : forall i, IsEquiv (diag_equiv_map i) }.

  Global Arguments diag_equiv_map [D1 D2] e : rename.
  Global Arguments diag_equiv_isequiv [D1 D2] e i : rename.
  Global Arguments Build_diagram_equiv [D1 D2] m H : rename.

  (** Inverse, section and retraction of equivalences of diagrams. *)

  Lemma diagram_equiv_inv {D1 D2 : Diagram G} (w : diagram_equiv D1 D2)
    : DiagramMap D2 D1.
H: Funext
G: Graph
D1, D2: Diagram G
w: diagram_equiv D1 D2
DiagramMap D2 D1
  Proof.
H: Funext
G: Graph
D1, D2: Diagram G
w: diagram_equiv D1 D2
DiagramMap D2 D1
    apply (Build_DiagramMap
             (fun i => (Build_Equiv _ _ _ (diag_equiv_isequiv w i))^-1)).
H: Funext
G: Graph
D1, D2: Diagram G
w: diagram_equiv D1 D2
forall (i j : G) (g : G i j) (x : D2 i),
(D1 _f g)
  ({|
     equiv_fun := w i;
     equiv_isequiv := diag_equiv_isequiv w i
   |}^-1 x) =
{|
  equiv_fun := w j;
  equiv_isequiv := diag_equiv_isequiv w j
|}^-1 ((D2 _f g) x)
    intros i j f.
H: Funext
G: Graph
D1, D2: Diagram G
w: diagram_equiv D1 D2
i, j: G
f: G i j
forall x : D2 i,
(D1 _f f)
  ({|
     equiv_fun := w i;
     equiv_isequiv := diag_equiv_isequiv w i
   |}^-1 x) =
{|
  equiv_fun := w j;
  equiv_isequiv := diag_equiv_isequiv w j
|}^-1 ((D2 _f f) x)
    apply (@comm_square_inverse _ _ _ _ _ _
                                (Build_Equiv _ _ _ (diag_equiv_isequiv w i))
                                (Build_Equiv _ _ _ (diag_equiv_isequiv w j))).
H: Funext
G: Graph
D1, D2: Diagram G
w: diagram_equiv D1 D2
i, j: G
f: G i j
(fun x : D1 i =>
 (D2 _f f)
   ({|
      equiv_fun := w i;
      equiv_isequiv := diag_equiv_isequiv w i
    |} x)) ==
(fun x : D1 i =>
 {|
   equiv_fun := w j;
   equiv_isequiv := diag_equiv_isequiv w j
 |} ((D1 _f f) x))
    intros x; apply DiagramMap_comm.
  Defined.

  Lemma diagram_inv_is_section {D1 D2 : Diagram G}
        (w : diagram_equiv D1 D2)
    : diagram_comp w (diagram_equiv_inv w) = diagram_idmap D2.
H: Funext
G: Graph
D1, D2: Diagram G
w: diagram_equiv D1 D2
diagram_comp w (diagram_equiv_inv w) =
diagram_idmap D2
  Proof.
H: Funext
G: Graph
D1, D2: Diagram G
w: diagram_equiv D1 D2
diagram_comp w (diagram_equiv_inv w) =
diagram_idmap D2
    destruct w as [[w_obj w_comm] is_eq_w].
H: Funext
G: Graph
D1, D2: Diagram G
w_obj: forall i : G, D1 i -> D2 i
w_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
(D2 _f g) (w_obj i x) = w_obj j ((D1 _f g) x)
is_eq_w: forall i : G,
IsEquiv
  ({|
     DiagramMap_obj := w_obj;
     DiagramMap_comm := w_comm
   |} i)
diagram_comp
  {|
    diag_equiv_map :=
      {|
        DiagramMap_obj := w_obj;
        DiagramMap_comm := w_comm
      |};
    diag_equiv_isequiv := is_eq_w
  |}
  (diagram_equiv_inv
     {|
       diag_equiv_map :=
         {|
           DiagramMap_obj := w_obj;
           DiagramMap_comm := w_comm
         |};
       diag_equiv_isequiv := is_eq_w
     |}) = diagram_idmap D2 simpl in *.
H: Funext
G: Graph
D1, D2: Diagram G
w_obj: forall i : G, D1 i -> D2 i
w_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
(D2 _f g) (w_obj i x) = w_obj j ((D1 _f g) x)
is_eq_w: forall i : G, IsEquiv (w_obj i)
diagram_comp
  {|
    DiagramMap_obj := w_obj; DiagramMap_comm := w_comm
  |}
  (diagram_equiv_inv
     {|
       diag_equiv_map :=
         {|
           DiagramMap_obj := w_obj;
           DiagramMap_comm := w_comm
         |};
       diag_equiv_isequiv := is_eq_w
     |}) = diagram_idmap D2
    set (we i := Build_Equiv _ _ _ (is_eq_w i)).
H: Funext
G: Graph
D1, D2: Diagram G
w_obj: forall i : G, D1 i -> D2 i
w_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
(D2 _f g) (w_obj i x) = w_obj j ((D1 _f g) x)
is_eq_w: forall i : G, IsEquiv (w_obj i)
we:= fun i : G =>
{|
  equiv_fun := w_obj i; equiv_isequiv := is_eq_w i
|}: forall i : G, D1 i <~> D2 i
diagram_comp
  {|
    DiagramMap_obj := w_obj; DiagramMap_comm := w_comm
  |}
  (diagram_equiv_inv
     {|
       diag_equiv_map :=
         {|
           DiagramMap_obj := w_obj;
           DiagramMap_comm := w_comm
         |};
       diag_equiv_isequiv := is_eq_w
     |}) = diagram_idmap D2
    simple refine (path_DiagramMap _ _).
H: Funext
G: Graph
D1, D2: Diagram G
w_obj: forall i : G, D1 i -> D2 i
w_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
(D2 _f g) (w_obj i x) = w_obj j ((D1 _f g) x)
is_eq_w: forall i : G, IsEquiv (w_obj i)
we:= fun i : G =>
{|
  equiv_fun := w_obj i; equiv_isequiv := is_eq_w i
|}: forall i : G, D1 i <~> D2 i
forall i : G,
diagram_comp
  {|
    DiagramMap_obj := w_obj; DiagramMap_comm := w_comm
  |}
  (diagram_equiv_inv
     {|
       diag_equiv_map :=
         {|
           DiagramMap_obj := w_obj;
           DiagramMap_comm := w_comm
         |};
       diag_equiv_isequiv := is_eq_w
     |}) i == diagram_idmap D2 i
H: Funext
G: Graph
D1, D2: Diagram G
w_obj: forall i : G, D1 i -> D2 i
w_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
(D2 _f g) (w_obj i x) = w_obj j ((D1 _f g) x)
is_eq_w: forall i : G, IsEquiv (w_obj i)
we:= fun i : G =>
{|
  equiv_fun := w_obj i; equiv_isequiv := is_eq_w i
|}: forall i : G, D1 i <~> D2 i
forall (i j : G) (g : G i j) 
(x : D2 i),
DiagramMap_comm
  (diagram_comp
     {|
       DiagramMap_obj := w_obj;
       DiagramMap_comm := w_comm
     |}
     (diagram_equiv_inv
        {|
          diag_equiv_map :=
            {|
              DiagramMap_obj := w_obj;
              DiagramMap_comm := w_comm
            |};
          diag_equiv_isequiv := is_eq_w
        |})) g x @ ?h_obj j ((D2 _f g) x) =
ap (D2 _f g) (?h_obj i x) @
DiagramMap_comm (diagram_idmap D2) g x
    -
H: Funext
G: Graph
D1, D2: Diagram G
w_obj: forall i : G, D1 i -> D2 i
w_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
(D2 _f g) (w_obj i x) = w_obj j ((D1 _f g) x)
is_eq_w: forall i : G, IsEquiv (w_obj i)
we:= fun i : G =>
{|
  equiv_fun := w_obj i; equiv_isequiv := is_eq_w i
|}: forall i : G, D1 i <~> D2 i
forall i : G,
diagram_comp
  {|
    DiagramMap_obj := w_obj; DiagramMap_comm := w_comm
  |}
  (diagram_equiv_inv
     {|
       diag_equiv_map :=
         {|
           DiagramMap_obj := w_obj;
           DiagramMap_comm := w_comm
         |};
       diag_equiv_isequiv := is_eq_w
     |}) i == diagram_idmap D2 i exact (fun i => eisretr (we i)).
    -
H: Funext
G: Graph
D1, D2: Diagram G
w_obj: forall i : G, D1 i -> D2 i
w_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
(D2 _f g) (w_obj i x) = w_obj j ((D1 _f g) x)
is_eq_w: forall i : G, IsEquiv (w_obj i)
we:= fun i : G =>
{|
  equiv_fun := w_obj i; equiv_isequiv := is_eq_w i
|}: forall i : G, D1 i <~> D2 i
forall (i j : G) (g : G i j) (x : D2 i),
DiagramMap_comm
  (diagram_comp
     {|
       DiagramMap_obj := w_obj;
       DiagramMap_comm := w_comm
     |}
     (diagram_equiv_inv
        {|
          diag_equiv_map :=
            {|
              DiagramMap_obj := w_obj;
              DiagramMap_comm := w_comm
            |};
          diag_equiv_isequiv := is_eq_w
        |})) g x @
(fun i0 : G =>
 eisretr
   {|
     equiv_fun :=
       {|
         diag_equiv_map :=
           {|
             DiagramMap_obj := w_obj;
             DiagramMap_comm := w_comm
           |};
         diag_equiv_isequiv := is_eq_w
       |} i0;
     equiv_isequiv :=
       diag_equiv_isequiv
         {|
           diag_equiv_map :=
             {|
               DiagramMap_obj := w_obj;
               DiagramMap_comm := w_comm
             |};
           diag_equiv_isequiv := is_eq_w
         |} i0
   |}) j ((D2 _f g) x) =
ap (D2 _f g)
  ((fun i0 : G =>
    eisretr
      {|
        equiv_fun :=
          {|
            diag_equiv_map :=
              {|
                DiagramMap_obj := w_obj;
                DiagramMap_comm := w_comm
              |};
            diag_equiv_isequiv := is_eq_w
          |} i0;
        equiv_isequiv :=
          diag_equiv_isequiv
            {|
              diag_equiv_map :=
                {|
                  DiagramMap_obj := w_obj;
                  DiagramMap_comm := w_comm
                |};
              diag_equiv_isequiv := is_eq_w
            |} i0
      |}) i x) @
DiagramMap_comm (diagram_idmap D2) g x simpl.
H: Funext
G: Graph
D1, D2: Diagram G
w_obj: forall i : G, D1 i -> D2 i
w_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
(D2 _f g) (w_obj i x) = w_obj j ((D1 _f g) x)
is_eq_w: forall i : G, IsEquiv (w_obj i)
we:= fun i : G =>
{|
  equiv_fun := w_obj i; equiv_isequiv := is_eq_w i
|}: forall i : G, D1 i <~> D2 i
forall (i j : G) (g : G i j) (x : D2 i),
comm_square_comp
  (comm_square_inverse
     (fun x0 : D1 i => w_comm i j g x0))
  (w_comm i j g) x @ eisretr (w_obj j) ((D2 _f g) x) =
ap (D2 _f g) (eisretr (w_obj i) x) @ 1
      intros i j f x.
H: Funext
G: Graph
D1, D2: Diagram G
w_obj: forall i : G, D1 i -> D2 i
w_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
(D2 _f g) (w_obj i x) = w_obj j ((D1 _f g) x)
is_eq_w: forall i : G, IsEquiv (w_obj i)
we:= fun i : G =>
{|
  equiv_fun := w_obj i; equiv_isequiv := is_eq_w i
|}: forall i : G, D1 i <~> D2 i
i, j: G
f: G i j
x: D2 i
comm_square_comp
  (comm_square_inverse
     (fun x : D1 i => w_comm i j f x)) (w_comm i j f)
  x @ eisretr (w_obj j) ((D2 _f f) x) =
ap (D2 _f f) (eisretr (w_obj i) x) @ 1 apply (concatR (concat_p1 _)^).
H: Funext
G: Graph
D1, D2: Diagram G
w_obj: forall i : G, D1 i -> D2 i
w_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
(D2 _f g) (w_obj i x) = w_obj j ((D1 _f g) x)
is_eq_w: forall i : G, IsEquiv (w_obj i)
we:= fun i : G =>
{|
  equiv_fun := w_obj i; equiv_isequiv := is_eq_w i
|}: forall i : G, D1 i <~> D2 i
i, j: G
f: G i j
x: D2 i
comm_square_comp
  (comm_square_inverse
     (fun x : D1 i => w_comm i j f x)) (w_comm i j f)
  x @ eisretr (w_obj j) ((D2 _f f) x) =
ap (D2 _f f) (eisretr (w_obj i) x)
      apply (comm_square_inverse_is_retr (we i) (we j) _ x).
  Defined.

  Lemma diagram_inv_is_retraction {D1 D2 : Diagram G}
        (w : diagram_equiv D1 D2)
    : diagram_comp (diagram_equiv_inv w) w = diagram_idmap D1.
H: Funext
G: Graph
D1, D2: Diagram G
w: diagram_equiv D1 D2
diagram_comp (diagram_equiv_inv w) w =
diagram_idmap D1
  Proof.
H: Funext
G: Graph
D1, D2: Diagram G
w: diagram_equiv D1 D2
diagram_comp (diagram_equiv_inv w) w =
diagram_idmap D1
    destruct w as [[w_obj w_comm] is_eq_w].
H: Funext
G: Graph
D1, D2: Diagram G
w_obj: forall i : G, D1 i -> D2 i
w_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
(D2 _f g) (w_obj i x) = w_obj j ((D1 _f g) x)
is_eq_w: forall i : G,
IsEquiv
  ({|
     DiagramMap_obj := w_obj;
     DiagramMap_comm := w_comm
   |} i)
diagram_comp
  (diagram_equiv_inv
     {|
       diag_equiv_map :=
         {|
           DiagramMap_obj := w_obj;
           DiagramMap_comm := w_comm
         |};
       diag_equiv_isequiv := is_eq_w
     |})
  {|
    diag_equiv_map :=
      {|
        DiagramMap_obj := w_obj;
        DiagramMap_comm := w_comm
      |};
    diag_equiv_isequiv := is_eq_w
  |} = diagram_idmap D1 simpl in *.
H: Funext
G: Graph
D1, D2: Diagram G
w_obj: forall i : G, D1 i -> D2 i
w_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
(D2 _f g) (w_obj i x) = w_obj j ((D1 _f g) x)
is_eq_w: forall i : G, IsEquiv (w_obj i)
diagram_comp
  (diagram_equiv_inv
     {|
       diag_equiv_map :=
         {|
           DiagramMap_obj := w_obj;
           DiagramMap_comm := w_comm
         |};
       diag_equiv_isequiv := is_eq_w
     |})
  {|
    DiagramMap_obj := w_obj; DiagramMap_comm := w_comm
  |} = diagram_idmap D1
    set (we i := Build_Equiv _ _ _ (is_eq_w i)).
H: Funext
G: Graph
D1, D2: Diagram G
w_obj: forall i : G, D1 i -> D2 i
w_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
(D2 _f g) (w_obj i x) = w_obj j ((D1 _f g) x)
is_eq_w: forall i : G, IsEquiv (w_obj i)
we:= fun i : G =>
{|
  equiv_fun := w_obj i; equiv_isequiv := is_eq_w i
|}: forall i : G, D1 i <~> D2 i
diagram_comp
  (diagram_equiv_inv
     {|
       diag_equiv_map :=
         {|
           DiagramMap_obj := w_obj;
           DiagramMap_comm := w_comm
         |};
       diag_equiv_isequiv := is_eq_w
     |})
  {|
    DiagramMap_obj := w_obj; DiagramMap_comm := w_comm
  |} = diagram_idmap D1
    simple refine (path_DiagramMap _ _).
H: Funext
G: Graph
D1, D2: Diagram G
w_obj: forall i : G, D1 i -> D2 i
w_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
(D2 _f g) (w_obj i x) = w_obj j ((D1 _f g) x)
is_eq_w: forall i : G, IsEquiv (w_obj i)
we:= fun i : G =>
{|
  equiv_fun := w_obj i; equiv_isequiv := is_eq_w i
|}: forall i : G, D1 i <~> D2 i
forall i : G,
diagram_comp
  (diagram_equiv_inv
     {|
       diag_equiv_map :=
         {|
           DiagramMap_obj := w_obj;
           DiagramMap_comm := w_comm
         |};
       diag_equiv_isequiv := is_eq_w
     |})
  {|
    DiagramMap_obj := w_obj; DiagramMap_comm := w_comm
  |} i == diagram_idmap D1 i
H: Funext
G: Graph
D1, D2: Diagram G
w_obj: forall i : G, D1 i -> D2 i
w_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
(D2 _f g) (w_obj i x) = w_obj j ((D1 _f g) x)
is_eq_w: forall i : G, IsEquiv (w_obj i)
we:= fun i : G =>
{|
  equiv_fun := w_obj i; equiv_isequiv := is_eq_w i
|}: forall i : G, D1 i <~> D2 i
forall (i j : G) (g : G i j) 
(x : D1 i),
DiagramMap_comm
  (diagram_comp
     (diagram_equiv_inv
        {|
          diag_equiv_map :=
            {|
              DiagramMap_obj := w_obj;
              DiagramMap_comm := w_comm
            |};
          diag_equiv_isequiv := is_eq_w
        |})
     {|
       DiagramMap_obj := w_obj;
       DiagramMap_comm := w_comm
     |}) g x @ ?h_obj j ((D1 _f g) x) =
ap (D1 _f g) (?h_obj i x) @
DiagramMap_comm (diagram_idmap D1) g x
    -
H: Funext
G: Graph
D1, D2: Diagram G
w_obj: forall i : G, D1 i -> D2 i
w_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
(D2 _f g) (w_obj i x) = w_obj j ((D1 _f g) x)
is_eq_w: forall i : G, IsEquiv (w_obj i)
we:= fun i : G =>
{|
  equiv_fun := w_obj i; equiv_isequiv := is_eq_w i
|}: forall i : G, D1 i <~> D2 i
forall i : G,
diagram_comp
  (diagram_equiv_inv
     {|
       diag_equiv_map :=
         {|
           DiagramMap_obj := w_obj;
           DiagramMap_comm := w_comm
         |};
       diag_equiv_isequiv := is_eq_w
     |})
  {|
    DiagramMap_obj := w_obj; DiagramMap_comm := w_comm
  |} i == diagram_idmap D1 i exact (fun i => eissect (we i)).
    -
H: Funext
G: Graph
D1, D2: Diagram G
w_obj: forall i : G, D1 i -> D2 i
w_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
(D2 _f g) (w_obj i x) = w_obj j ((D1 _f g) x)
is_eq_w: forall i : G, IsEquiv (w_obj i)
we:= fun i : G =>
{|
  equiv_fun := w_obj i; equiv_isequiv := is_eq_w i
|}: forall i : G, D1 i <~> D2 i
forall (i j : G) (g : G i j) (x : D1 i),
DiagramMap_comm
  (diagram_comp
     (diagram_equiv_inv
        {|
          diag_equiv_map :=
            {|
              DiagramMap_obj := w_obj;
              DiagramMap_comm := w_comm
            |};
          diag_equiv_isequiv := is_eq_w
        |})
     {|
       DiagramMap_obj := w_obj;
       DiagramMap_comm := w_comm
     |}) g x @
(fun i0 : G =>
 eissect
   {|
     equiv_fun :=
       {|
         diag_equiv_map :=
           {|
             DiagramMap_obj := w_obj;
             DiagramMap_comm := w_comm
           |};
         diag_equiv_isequiv := is_eq_w
       |} i0;
     equiv_isequiv :=
       diag_equiv_isequiv
         {|
           diag_equiv_map :=
             {|
               DiagramMap_obj := w_obj;
               DiagramMap_comm := w_comm
             |};
           diag_equiv_isequiv := is_eq_w
         |} i0
   |}) j ((D1 _f g) x) =
ap (D1 _f g)
  ((fun i0 : G =>
    eissect
      {|
        equiv_fun :=
          {|
            diag_equiv_map :=
              {|
                DiagramMap_obj := w_obj;
                DiagramMap_comm := w_comm
              |};
            diag_equiv_isequiv := is_eq_w
          |} i0;
        equiv_isequiv :=
          diag_equiv_isequiv
            {|
              diag_equiv_map :=
                {|
                  DiagramMap_obj := w_obj;
                  DiagramMap_comm := w_comm
                |};
              diag_equiv_isequiv := is_eq_w
            |} i0
      |}) i x) @
DiagramMap_comm (diagram_idmap D1) g x simpl.
H: Funext
G: Graph
D1, D2: Diagram G
w_obj: forall i : G, D1 i -> D2 i
w_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
(D2 _f g) (w_obj i x) = w_obj j ((D1 _f g) x)
is_eq_w: forall i : G, IsEquiv (w_obj i)
we:= fun i : G =>
{|
  equiv_fun := w_obj i; equiv_isequiv := is_eq_w i
|}: forall i : G, D1 i <~> D2 i
forall (i j : G) (g : G i j) (x : D1 i),
comm_square_comp (w_comm i j g)
  (comm_square_inverse
     (fun x0 : D1 i => w_comm i j g x0)) x @
eissect (w_obj j) ((D1 _f g) x) =
ap (D1 _f g) (eissect (w_obj i) x) @ 1
      intros i j f x.
H: Funext
G: Graph
D1, D2: Diagram G
w_obj: forall i : G, D1 i -> D2 i
w_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
(D2 _f g) (w_obj i x) = w_obj j ((D1 _f g) x)
is_eq_w: forall i : G, IsEquiv (w_obj i)
we:= fun i : G =>
{|
  equiv_fun := w_obj i; equiv_isequiv := is_eq_w i
|}: forall i : G, D1 i <~> D2 i
i, j: G
f: G i j
x: D1 i
comm_square_comp (w_comm i j f)
  (comm_square_inverse
     (fun x : D1 i => w_comm i j f x)) x @
eissect (w_obj j) ((D1 _f f) x) =
ap (D1 _f f) (eissect (w_obj i) x) @ 1 apply (concatR (concat_p1 _)^).
H: Funext
G: Graph
D1, D2: Diagram G
w_obj: forall i : G, D1 i -> D2 i
w_comm: forall (i j : G) (g : G i j) 
(x : D1 i),
(D2 _f g) (w_obj i x) = w_obj j ((D1 _f g) x)
is_eq_w: forall i : G, IsEquiv (w_obj i)
we:= fun i : G =>
{|
  equiv_fun := w_obj i; equiv_isequiv := is_eq_w i
|}: forall i : G, D1 i <~> D2 i
i, j: G
f: G i j
x: D1 i
comm_square_comp (w_comm i j f)
  (comm_square_inverse
     (fun x : D1 i => w_comm i j f x)) x @
eissect (w_obj j) ((D1 _f f) x) =
ap (D1 _f f) (eissect (w_obj i) x)
      apply (comm_square_inverse_is_sect (we i) (we j) _ x).
  Defined.

  (** The equivalence of diagram is an equivalence relation. *)
  (** Those instances allows to use the tactics reflexivity, symmetry and transitivity. *)
  Global Instance reflexive_diagram_equiv : Reflexive diagram_equiv | 1
    := fun D => Build_diagram_equiv (diagram_idmap D) _.

  Global Instance symmetric_diagram_equiv : Symmetric diagram_equiv | 1
    := fun D1 D2 m => Build_diagram_equiv (diagram_equiv_inv m) _.

  Global Instance transitive_diagram_equiv : Transitive diagram_equiv | 1.
H: Funext
G: Graph
Transitive diagram_equiv
  Proof.
H: Funext
G: Graph
Transitive diagram_equiv
  simple refine (fun D1 D2 D3 m1 m2 =>
                   Build_diagram_equiv (diagram_comp m2 m1) _).
H: Funext
G: Graph
D1, D2, D3: Diagram G
m1: diagram_equiv D1 D2
m2: diagram_equiv D2 D3
forall i : G, IsEquiv (diagram_comp m2 m1 i)
  simpl.
H: Funext
G: Graph
D1, D2, D3: Diagram G
m1: diagram_equiv D1 D2
m2: diagram_equiv D2 D3
forall i : G, IsEquiv (fun x : D1 i => m2 i (m1 i x)) intros i; apply isequiv_compose';[apply m1 | apply m2].
  Defined.
End Diagram.

Notation "D1 ~d~ D2" := (diagram_equiv D1 D2).