From HoTT Require Import Basics.From HoTT Require Import Basics.
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 i0 : G, D1 i0 = D2 i0
path_arr: forall (i0 j : G) (g : G i0 j) (x : D1 i0),
transport idmap (path_obj j) ((D1 _f g) x) =
(D2 _f g) (transport idmap (path_obj i0) x)
i: G
D1 i = D2 i
H: Funext
G: Graph
D1, D2: Diagram G
path_obj: forall i0 : G, D1 i0 = D2 i0
path_arr: forall (i0 j : G) (g : G i0 j) (x : D1 i0),
transport idmap (path_obj j) ((D1 _f g) x) =
(D2 _f g) (transport idmap (path_obj i0) x)
i: G
transport (fun D' : G -> Type => forall i0 j : G, G i0 j -> D' i0 -> D' j)
  (path_forall D1 D2 (fun i0 : G => ?Goal@{i:=i0})) 
  (arr D1) i =
arr D2 (i:=i)
    1: apply path_obj.
H: Funext
G: Graph
D1, D2: Diagram G
path_obj: forall i0 : G, D1 i0 = D2 i0
path_arr: forall (i0 j : G) (g : G i0 j) (x : D1 i0),
transport idmap (path_obj j) ((D1 _f g) x) =
(D2 _f g) (transport idmap (path_obj i0) x)
i: G
transport (fun D' : G -> Type => forall i0 j : G, G i0 j -> D' i0 -> D' j)
  (path_forall D1 D2 (fun i0 : G => path_obj i0)) 
  (arr D1) i =
arr D2 (i:=i)
    funext j g x.
H: Funext
G: Graph
D1, D2: Diagram G
path_obj: forall i0 : G, D1 i0 = D2 i0
path_arr: forall (i0 j0 : G) (g0 : G i0 j0) (x0 : D1 i0),
transport idmap (path_obj j0) ((D1 _f g0) x0) =
(D2 _f g0) (transport idmap (path_obj i0) x0)
i, j: G
g: G i j
x: D2 i
transport (fun D' : G -> Type => forall i0 j0 : G, G i0 j0 -> D' i0 -> D' j0)
  (path_forall D1 D2 (fun i0 : G => path_obj i0)) 
  (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 i0 : G, D1 i0 = D2 i0
path_arr: forall (i0 j0 : G) (g0 : G i0 j0) (x0 : D1 i0),
transport idmap (path_obj j0) ((D1 _f g0) x0) =
(D2 _f g0) (transport idmap (path_obj i0) x0)
i, j: G
g: G i j
x: D2 i
transport (fun x0 : G -> Type => x0 j)
  (path_forall D1 D2 (fun i0 : G => path_obj i0))
  ((D1 _f g)
     (transport (fun x0 : G -> Type => x0 i)
        (path_forall D1 D2 (fun i0 : G => path_obj i0))^ x)) =
(D2 _f g) x
    transport_path_forall_hammer.
H: Funext
G: Graph
D1, D2: Diagram G
path_obj: forall i0 : G, D1 i0 = D2 i0
path_arr: forall (i0 j0 : G) (g0 : G i0 j0) (x0 : D1 i0),
transport idmap (path_obj j0) ((D1 _f g0) x0) =
(D2 _f g0) (transport idmap (path_obj i0) x0)
i, j: G
g: G i j
x: D2 i
transport idmap (path_obj j)
  ((D1 _f g)
     (transport (fun x0 : G -> Type => x0 i)
        (path_forall D1 D2 (fun i0 : G => path_obj i0))^ 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 i0 : G, D1 i0 = D2 i0
path_arr: forall (i0 j0 : G) (g0 : G i0 j0) (x0 : D1 i0),
transport idmap (path_obj j0) ((D1 _f g0) x0) =
(D2 _f g0) (transport idmap (path_obj i0) x0)
i, j: G
g: G i j
x: D2 i
transport idmap (path_obj j)
  ((D1 _f g)
     (transport (fun x0 : G -> Type => x0 i)
        (path_forall D1 D2 (fun i0 : G => path_obj i0))^ 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 i0 : G, D1 i0 = D2 i0
path_arr: forall (i0 j0 : G) (g0 : G i0 j0) (x0 : D1 i0),
transport idmap (path_obj j0) ((D1 _f g0) x0) =
(D2 _f g0) (transport idmap (path_obj i0) x0)
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 i0 : G, D1 i0 = D2 i0
path_arr: forall (i0 j0 : G) (g0 : G i0 j0) (x0 : D1 i0),
transport idmap (path_obj j0) ((D1 _f g0) x0) =
(D2 _f g0) (transport idmap (path_obj i0) x0)
i, j: G
g: G i j
x: D2 i
transport idmap (path_obj j)
  ((D1 _f g)
     (transport (fun x0 : G -> Type => x0 i)
        (path_forall D1 D2 (fun i0 : G => path_obj i0))^ 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 i0 : G, D1 i0 = D2 i0
path_arr: forall (i0 j0 : G) (g0 : G i0 j0) (x0 : D1 i0),
transport idmap (path_obj j0) ((D1 _f g0) x0) =
(D2 _f g0) (transport idmap (path_obj i0) x0)
i, j: G
g: G i j
x: D2 i
transport (fun x0 : G -> Type => x0 i)
  (path_forall D1 D2 (fun i0 : G => path_obj i0))^ =
transport idmap (path_obj i)^
      rewrite <- path_forall_V.
H: Funext
G: Graph
D1, D2: Diagram G
path_obj: forall i0 : G, D1 i0 = D2 i0
path_arr: forall (i0 j0 : G) (g0 : G i0 j0) (x0 : D1 i0),
transport idmap (path_obj j0) ((D1 _f g0) x0) =
(D2 _f g0) (transport idmap (path_obj i0) x0)
i, j: G
g: G i j
x: D2 i
transport (fun x0 : G -> Type => x0 i)
  (path_forall D2 D1 (fun x0 : G => (path_obj x0)^)) =
transport idmap (path_obj i)^
      funext y.
H: Funext
G: Graph
D1, D2: Diagram G
path_obj: forall i0 : G, D1 i0 = D2 i0
path_arr: forall (i0 j0 : G) (g0 : G i0 j0) (x0 : D1 i0),
transport idmap (path_obj j0) ((D1 _f g0) x0) =
(D2 _f g0) (transport idmap (path_obj i0) x0)
i, j: G
g: G i j
x, y: D2 i
transport (fun x0 : G -> Type => x0 i)
  (path_forall D2 D1 (fun x0 : G => (path_obj x0)^)) y =
transport idmap (path_obj i)^ y
      by transport_path_forall_hammer. }
H: Funext
G: Graph
D1, D2: Diagram G
path_obj: forall i0 : G, D1 i0 = D2 i0
path_arr: forall (i0 j0 : G) (g0 : G i0 j0) (x0 : D1 i0),
transport idmap (path_obj j0) ((D1 _f g0) x0) =
(D2 _f g0) (transport idmap (path_obj i0) x0)
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 i0 : G, D1 i0 = D2 i0
path_arr: forall (i0 j0 : G) (g0 : G i0 j0) (x0 : D1 i0),
transport idmap (path_obj j0) ((D1 _f g0) x0) =
(D2 _f g0) (transport idmap (path_obj i0) x0)
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 i0 : G, D1 i0 -> D2 i0
m1_comm, m2_comm: forall (i0 j0 : G) (g : G i0 j0) (x0 : D1 i0),
(D2 _f g) (m1_obj i0 x0) = m1_obj j0 ((D1 _f g) x0)
E:= equiv_functor_forall idmap (fun i0 : G => apD10): (forall a : G, m1_obj a = m1_obj a) <~> (forall b : G, m1_obj b == m1_obj b)
h_comm: forall (i0 j0 : G) (g : G i0 j0) (x0 : D1 i0),
m1_comm i0 j0 g x0 @
functor_forall idmap (fun i1 : G => apD10) (apD10 1) j0 ((D1 _f g) x0) =
1 @ m2_comm i0 j0 g x0
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 i0 : G, D1 i0 -> D2 i0
m1_comm, m2_comm: forall (i0 j0 : G) (g : G i0 j0) (x0 : D1 i0),
(D2 _f g) (m1_obj i0 x0) = m1_obj j0 ((D1 _f g) x0)
E:= equiv_functor_forall idmap (fun i0 : G => apD10): (forall a : G, m1_obj a = m1_obj a) <~> (forall b : G, m1_obj b == m1_obj b)
h_comm: forall (i0 j0 : G) (g : G i0 j0) (x0 : D1 i0),
m1_comm i0 j0 g x0 @
functor_forall idmap (fun i1 : G => apD10) (apD10 1) j0 ((D1 _f g) x0) =
1 @ m2_comm i0 j0 g x0
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 i0 : G, D1 i0 -> D2 i0
m1_comm, m2_comm: forall (i0 j0 : G) (g : G i0 j0) (x0 : D1 i0),
(D2 _f g) (m1_obj i0 x0) = m1_obj j0 ((D1 _f g) x0)
E:= equiv_functor_forall idmap (fun i0 : G => apD10): (forall a : G, m1_obj a = m1_obj a) <~> (forall b : G, m1_obj b == m1_obj b)
h_comm: forall (i0 j0 : G) (g : G i0 j0) (x0 : D1 i0),
m1_comm i0 j0 g x0 @
functor_forall idmap (fun i1 : G => apD10) (apD10 1) j0 ((D1 _f g) x0) =
1 @ m2_comm i0 j0 g x0
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 i0 : 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 i0 : G, D1 i0 -> D2 i0
w_comm: forall (i0 j0 : G) (g : G i0 j0) (x0 : D1 i0),
(D2 _f g) (w_obj i0 x0) = w_obj j0 ((D1 _f g) x0)
is_eq_w: forall i0 : G, IsEquiv (w_obj i0)
we:= fun i0 : G => {| equiv_fun := w_obj i0; equiv_isequiv := is_eq_w i0 |}: forall i0 : G, D1 i0 <~> D2 i0
i, j: G
f: G i j
x: D2 i
comm_square_comp (comm_square_inverse (fun x0 : D1 i => w_comm i j f x0))
  (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 i0 : G, D1 i0 -> D2 i0
w_comm: forall (i0 j0 : G) (g : G i0 j0) (x0 : D1 i0),
(D2 _f g) (w_obj i0 x0) = w_obj j0 ((D1 _f g) x0)
is_eq_w: forall i0 : G, IsEquiv (w_obj i0)
we:= fun i0 : G => {| equiv_fun := w_obj i0; equiv_isequiv := is_eq_w i0 |}: forall i0 : G, D1 i0 <~> D2 i0
i, j: G
f: G i j
x: D2 i
comm_square_comp (comm_square_inverse (fun x0 : D1 i => w_comm i j f x0))
  (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 i0 : G, D1 i0 -> D2 i0
w_comm: forall (i0 j0 : G) (g : G i0 j0) (x0 : D1 i0),
(D2 _f g) (w_obj i0 x0) = w_obj j0 ((D1 _f g) x0)
is_eq_w: forall i0 : G, IsEquiv (w_obj i0)
we:= fun i0 : G => {| equiv_fun := w_obj i0; equiv_isequiv := is_eq_w i0 |}: forall i0 : G, D1 i0 <~> D2 i0
i, j: G
f: G i j
x: D1 i
comm_square_comp (w_comm i j f)
  (comm_square_inverse (fun x0 : D1 i => w_comm i j f x0)) 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 i0 : G, D1 i0 -> D2 i0
w_comm: forall (i0 j0 : G) (g : G i0 j0) (x0 : D1 i0),
(D2 _f g) (w_obj i0 x0) = w_obj j0 ((D1 _f g) x0)
is_eq_w: forall i0 : G, IsEquiv (w_obj i0)
we:= fun i0 : G => {| equiv_fun := w_obj i0; equiv_isequiv := is_eq_w i0 |}: forall i0 : G, D1 i0 <~> D2 i0
i, j: G
f: G i j
x: D1 i
comm_square_comp (w_comm i j f)
  (comm_square_inverse (fun x0 : D1 i => w_comm i j f x0)) 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).