Diagram.v

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] _ _.

  Definition DiagramMap_homotopy {D1 D2 : Diagram G}
    (m1 m2 : DiagramMap D1 D2) : Type
    := {h_obj : (forall i, m1 i == m2 i) & (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)}.

  #[export] Instance reflexive_DiagramMap_homotopy {D1 D2 : Diagram G} : Reflexive (@DiagramMap_homotopy D1 D2).H: Funext
G: Graph
D1, D2: Diagram G
Reflexive DiagramMap_homotopy
  Proof.H: Funext
G: Graph
D1, D2: Diagram G
Reflexive DiagramMap_homotopy
    intros m.H: Funext
G: Graph
D1, D2: Diagram G
m: DiagramMap D1 D2
DiagramMap_homotopy m m
    snapply exist.H: Funext
G: Graph
D1, D2: Diagram G
m: DiagramMap D1 D2
forall i : G, m i == m i
H: Funext
G: Graph
D1, D2: Diagram G
m: DiagramMap D1 D2
(fun h_obj : forall i : G, m i == m i =>
 forall (i j : G) (g : G i j) (x : D1 i),
 DiagramMap_comm m g x @ h_obj j ((D1 _f g) x) =
 ap (D2 _f g) (h_obj i x) @ DiagramMap_comm m g x)
  ?proj1
    -H: Funext
G: Graph
D1, D2: Diagram G
m: DiagramMap D1 D2
forall i : G, m i == m i intro i; reflexivity.
    -H: Funext
G: Graph
D1, D2: Diagram G
m: DiagramMap D1 D2
(fun h_obj : forall i : G, m i == m i =>
 forall (i j : G) (g : G i j) (x : D1 i),
 DiagramMap_comm m g x @ h_obj j ((D1 _f g) x) =
 ap (D2 _f g) (h_obj i x) @ DiagramMap_comm m g x)
  (fun (i : G) (x0 : D1 i) => 1) intros i j g x; cbn.H: Funext
G: Graph
D1, D2: Diagram G
m: DiagramMap D1 D2
i, j: G
g: G i j
x: D1 i
DiagramMap_comm m g x @ 1 = 1 @ DiagramMap_comm m g x
      apply concat_p1_1p.
  Defined.

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

  Definition path_DiagramMap {D1 D2 : Diagram G}
    {m1 m2 : DiagramMap D1 D2} (h : DiagramMap_homotopy m1 m2)
    : m1 = m2.H: Funext
G: Graph
D1, D2: Diagram G
m1, m2: DiagramMap D1 D2
h: DiagramMap_homotopy m1 m2
m1 = m2
  Proof.H: Funext
G: Graph
D1, D2: Diagram G
m1, m2: DiagramMap D1 D2
h: DiagramMap_homotopy m1 m2
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: DiagramMap_homotopy
  {|
    DiagramMap_obj := m1_obj;
    DiagramMap_comm := m1_comm
  |} m2
{|
  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: DiagramMap_homotopy
  {|
    DiagramMap_obj := m1_obj;
    DiagramMap_comm := m1_comm
  |}
  {|
    DiagramMap_obj := m2_obj;
    DiagramMap_comm := m2_comm
  |}
{|
  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: DiagramMap_homotopy
  {|
    DiagramMap_obj := m1_obj;
    DiagramMap_comm := m1_comm
  |}
  {|
    DiagramMap_obj := m2_obj;
    DiagramMap_comm := m2_comm
  |}
{|
  DiagramMap_obj := m1_obj; DiagramMap_comm := m1_comm
|} =
{|
  DiagramMap_obj := m2_obj; DiagramMap_comm := m2_comm
|}
    destruct h as [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)
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
|}
    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,
        {|
          DiagramMap_obj := m1_obj;
          DiagramMap_comm := m1_comm
        |} i ==
        {|
          DiagramMap_obj := m2_obj;
          DiagramMap_comm := m2_comm
        |} i,
(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
|}
    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,
        {|
          DiagramMap_obj := m1_obj;
          DiagramMap_comm := m1_comm
        |} i ==
        {|
          DiagramMap_obj := m2_obj;
          DiagramMap_comm := m2_comm
        |} i,
(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
|}
    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),
 DiagramMap_comm
   {|
     DiagramMap_obj := m1_obj;
     DiagramMap_comm := m1_comm
   |} g x @ E h_obj j ((D1 _f g) x) =
 ap (D2 _f g) (E 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
|}
    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),
 DiagramMap_comm
   {|
     DiagramMap_obj := m1_obj;
     DiagramMap_comm := m1_comm
   |} g x @ E h_obj j ((D1 _f g) x) =
 ap (D2 _f g) (E 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
|}
    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),
 DiagramMap_comm
   {|
     DiagramMap_obj := m1_obj;
     DiagramMap_comm := m1_comm
   |} g x @ E (apD10 h_obj) j ((D1 _f g) x) =
 ap (D2 _f g) (E (apD10 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
|}
    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
      rhs_V napply 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
      rhs_V napply 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
    apply 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
DiagramMap_homotopy
  (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)
    exists (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 @
eisretr
  {|
    equiv_fun :=
      {|
        diag_equiv_map :=
          {|
            DiagramMap_obj := w_obj;
            DiagramMap_comm := w_comm
          |};
        diag_equiv_isequiv := is_eq_w
      |} j;
    equiv_isequiv :=
      diag_equiv_isequiv
        {|
          diag_equiv_map :=
            {|
              DiagramMap_obj := w_obj;
              DiagramMap_comm := w_comm
            |};
          diag_equiv_isequiv := is_eq_w
        |} j
  |} ((D2 _f g) x) =
ap (D2 _f g)
  (eisretr
     {|
       equiv_fun :=
         {|
           diag_equiv_map :=
             {|
               DiagramMap_obj := w_obj;
               DiagramMap_comm := w_comm
             |};
           diag_equiv_isequiv := is_eq_w
         |} i;
       equiv_isequiv :=
         diag_equiv_isequiv
           {|
             diag_equiv_map :=
               {|
                 DiagramMap_obj := w_obj;
                 DiagramMap_comm := w_comm
               |};
             diag_equiv_isequiv := is_eq_w
           |} 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
    rhs napply 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)
    exact (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
    apply 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
DiagramMap_homotopy
  (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)
    exists (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 @
eissect
  {|
    equiv_fun :=
      {|
        diag_equiv_map :=
          {|
            DiagramMap_obj := w_obj;
            DiagramMap_comm := w_comm
          |};
        diag_equiv_isequiv := is_eq_w
      |} j;
    equiv_isequiv :=
      diag_equiv_isequiv
        {|
          diag_equiv_map :=
            {|
              DiagramMap_obj := w_obj;
              DiagramMap_comm := w_comm
            |};
          diag_equiv_isequiv := is_eq_w
        |} j
  |} ((D1 _f g) x) =
ap (D1 _f g)
  (eissect
     {|
       equiv_fun :=
         {|
           diag_equiv_map :=
             {|
               DiagramMap_obj := w_obj;
               DiagramMap_comm := w_comm
             |};
           diag_equiv_isequiv := is_eq_w
         |} i;
       equiv_isequiv :=
         diag_equiv_isequiv
           {|
             diag_equiv_map :=
               {|
                 DiagramMap_obj := w_obj;
                 DiagramMap_comm := w_comm
               |};
             diag_equiv_isequiv := is_eq_w
           |} 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
    rhs napply 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)
    exact (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. *)
  #[export] Instance reflexive_diagram_equiv : Reflexive diagram_equiv | 1
    := fun D => Build_diagram_equiv (diagram_idmap D) _.

  #[export] Instance symmetric_diagram_equiv : Symmetric diagram_equiv | 1
    := fun D1 D2 m => Build_diagram_equiv (diagram_equiv_inv m) _.

  #[export] Instance transitive_diagram_equiv : Transitive diagram_equiv | 1.H: Funext
G: Graph
Transitive diagram_equiv
  Proof.H: Funext
G: Graph
Transitive diagram_equiv
    intros D1 D2 D3 m1 m2.H: Funext
G: Graph
D1, D2, D3: Diagram G
m1: diagram_equiv D1 D2
m2: diagram_equiv D2 D3
diagram_equiv D1 D3
    napply (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)
    intros i.H: Funext
G: Graph
D1, D2, D3: Diagram G
m1: diagram_equiv D1 D2
m2: diagram_equiv D2 D3
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
i: G
IsEquiv (fun x : D1 i => m2 i (m1 i x))
    apply isequiv_compose; [apply m1 | apply m2].
  Defined.
End Diagram.

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