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

(** * Constant diagram *)

Section ConstantDiagram.

  Context {G : Graph}.

  Definition diagram_const (C : Type) : Diagram G.
G: Graph
C: Type
Diagram G
  Proof.
G: Graph
C: Type
Diagram G
    srapply Build_Diagram.
G: Graph
C: Type
G -> Type
G: Graph
C: Type
forall i j : G, G i j -> ?obj i -> ?obj j
    1: exact (fun _ => C).
G: Graph
C: Type
forall i j : G,
G i j -> (fun _ : G => C) i -> (fun _ : G => C) j
    intros i j k.
G: Graph
C: Type
i, j: G
k: G i j
(fun _ : G => C) i -> (fun _ : G => C) j
    exact idmap.
  Defined.

  Definition diagram_const_functor {A B : Type} (f : A -> B)
    : DiagramMap (diagram_const A) (diagram_const B).
G: Graph
A, B: Type
f: A -> B
DiagramMap (diagram_const A) (diagram_const B)
  Proof.
G: Graph
A, B: Type
f: A -> B
DiagramMap (diagram_const A) (diagram_const B)
    srapply Build_DiagramMap.
G: Graph
A, B: Type
f: A -> B
forall i : G, diagram_const A i -> diagram_const B i
G: Graph
A, B: Type
f: A -> B
forall (i j : G) (g : G i j) (x : diagram_const A i),
((diagram_const B) _f g) (?DiagramMap_obj i x) =
?DiagramMap_obj j (((diagram_const A) _f g) x)
    1: intro i; exact f.
G: Graph
A, B: Type
f: A -> B
forall (i j : G) (g : G i j) (x : diagram_const A i),
((diagram_const B) _f g) ((fun _ : G => f) i x) =
(fun _ : G => f) j (((diagram_const A) _f g) x)
    reflexivity.
  Defined.

  Definition diagram_const_functor_comp {A B C : Type}
    (f : A -> B) (g : B -> C)
    : diagram_const_functor (g o f)
    = diagram_comp (diagram_const_functor g) (diagram_const_functor f).
G: Graph
A, B, C: Type
f: A -> B
g: B -> C
diagram_const_functor (g o f) =
diagram_comp (diagram_const_functor g)
  (diagram_const_functor f)
  Proof.
G: Graph
A, B, C: Type
f: A -> B
g: B -> C
diagram_const_functor (g o f) =
diagram_comp (diagram_const_functor g)
  (diagram_const_functor f)
    reflexivity.
  Defined.

  Definition diagram_const_functor_idmap {A : Type}
    : diagram_const_functor (idmap : A -> A) = diagram_idmap (diagram_const A).
G: Graph
A: Type
diagram_const_functor (idmap : A -> A) =
diagram_idmap (diagram_const A)
  Proof.
G: Graph
A: Type
diagram_const_functor (idmap : A -> A) =
diagram_idmap (diagram_const A)
    reflexivity.
  Defined.

  Definition equiv_diagram_const_cocone `{Funext} (D : Diagram G) (X : Type)
    : DiagramMap D (diagram_const X) <~> Cocone D X.
G: Graph
H: Funext
D: Diagram G
X: Type
DiagramMap D (diagram_const X) <~> Cocone D X
  Proof.
G: Graph
H: Funext
D: Diagram G
X: Type
DiagramMap D (diagram_const X) <~> Cocone D X
    srapply equiv_adjointify.
G: Graph
H: Funext
D: Diagram G
X: Type
DiagramMap D (diagram_const X) -> Cocone D X
G: Graph
H: Funext
D: Diagram G
X: Type
Cocone D X -> DiagramMap D (diagram_const X)
G: Graph
H: Funext
D: Diagram G
X: Type
?f o ?g == idmap
G: Graph
H: Funext
D: Diagram G
X: Type
?g o ?f == idmap
    1,2: intros [? w]; econstructor.
G: Graph
H: Funext
D: Diagram G
X: Type
DiagramMap_obj: forall i : G,
D i -> diagram_const X i
w: forall (i j : G) (g : G i j) 
(x : D i),
((diagram_const X) _f g) (DiagramMap_obj i x) =
DiagramMap_obj j ((D _f g) x)
forall (i j : G) (g : G i j),
(fun x : D i => ?legs j ((D _f g) x)) == ?legs i
G: Graph
H: Funext
D: Diagram G
X: Type
legs: forall i : G, D i -> X
w: forall (i j : G) (g : G i j),
(fun x : D i => legs j ((D _f g) x)) == legs i
forall (i j : G) (g : G i j) 
(x : D i),
((diagram_const X) _f g) (?DiagramMap_obj i x) =
?DiagramMap_obj j ((D _f g) x)
G: Graph
H: Funext
D: Diagram G
X: Type
(fun X0 : DiagramMap D (diagram_const X) =>
 (fun
    (DiagramMap_obj : 
     forall i : G, D i -> diagram_const X i)
    (w : forall (i j : G) 
         (g : G i j) 
         (x : D i),
         ((diagram_const X) _f g) (DiagramMap_obj i x) =
         DiagramMap_obj j ((D _f g) x)) =>
  {| legs := ?legs; legs_comm := ?Goal |}) X0
   (DiagramMap_comm X0))
o (fun X0 : Cocone D X =>
   (fun (legs : forall i : G, D i -> X)
      (w : forall (i j : G) 
           (g : G i j),
           (fun x : D i => legs j ((D _f g) x)) ==
           legs i) =>
    {|
      DiagramMap_obj := ?DiagramMap_obj;
      DiagramMap_comm := ?Goal0
    |}) X0 (legs_comm X0)) == idmap
G: Graph
H: Funext
D: Diagram G
X: Type
(fun X0 : Cocone D X =>
 (fun (legs : forall i : G, D i -> X)
    (w : forall (i j : G) 
         (g : G i j),
         (fun x : D i => legs j ((D _f g) x)) ==
         legs i) =>
  {|
    DiagramMap_obj := ?DiagramMap_obj;
    DiagramMap_comm := ?Goal0
  |}) X0 (legs_comm X0))
o (fun X0 : DiagramMap D (diagram_const X) =>
   (fun
      (DiagramMap_obj : 
       forall i : G, 
       D i -> diagram_const X i)
      (w : forall (i j : G) 
           (g : G i j) 
           (x : D i),
           ((diagram_const X) _f g)
             (DiagramMap_obj i x) =
           DiagramMap_obj j ((D _f g) x)) =>
    {| legs := ?legs; legs_comm := ?Goal |}) X0
     (DiagramMap_comm X0)) == idmap
    1,2: intros x y z z'; symmetry; revert x y z z'.
G: Graph
H: Funext
D: Diagram G
X: Type
DiagramMap_obj: forall i : G,
D i -> diagram_const X i
w: forall (i j : G) (g : G i j) 
(x : D i),
((diagram_const X) _f g) (DiagramMap_obj i x) =
DiagramMap_obj j ((D _f g) x)
forall (x y : G) (z : G x y) (z' : D x),
?legs x z' = ?legs y ((D _f z) z')
G: Graph
H: Funext
D: Diagram G
X: Type
legs: forall i : G, D i -> X
w: forall (i j : G) (g : G i j),
(fun x : D i => legs j ((D _f g) x)) == legs i
forall (x y : G) (z : G x y) 
(z' : D x),
?DiagramMap_obj y ((D _f z) z') =
((diagram_const X) _f z) (?DiagramMap_obj x z')
G: Graph
H: Funext
D: Diagram G
X: Type
(fun X0 : DiagramMap D (diagram_const X) =>
 (fun
    (DiagramMap_obj : 
     forall i : G, D i -> diagram_const X i)
    (w : forall (i j : G) 
         (g : G i j) 
         (x : D i),
         ((diagram_const X) _f g) (DiagramMap_obj i x) =
         DiagramMap_obj j ((D _f g) x)) =>
  {|
    legs := ?legs;
    legs_comm :=
      fun (x y : G) (z : G x y) =>
      (fun z' : D x => (?Goal x y z z')^)
      :
      (fun x0 : D x => ?legs y ((D _f z) x0)) ==
      ?legs x
  |}) X0 (DiagramMap_comm X0))
o (fun X0 : Cocone D X =>
   (fun (legs : forall i : G, D i -> X)
      (w : forall (i j : G) 
           (g : G i j),
           (fun x : D i => legs j ((D _f g) x)) ==
           legs i) =>
    {|
      DiagramMap_obj := ?DiagramMap_obj;
      DiagramMap_comm :=
        fun (x y : G) (z : G x y) (z' : D x) =>
        (?Goal0 x y z z')^
    |}) X0 (legs_comm X0)) == idmap
G: Graph
H: Funext
D: Diagram G
X: Type
(fun X0 : Cocone D X =>
 (fun (legs : forall i : G, D i -> X)
    (w : forall (i j : G) 
         (g : G i j),
         (fun x : D i => legs j ((D _f g) x)) ==
         legs i) =>
  {|
    DiagramMap_obj := ?DiagramMap_obj;
    DiagramMap_comm :=
      fun (x y : G) (z : G x y) (z' : D x) =>
      (?Goal0 x y z z')^
  |}) X0 (legs_comm X0))
o (fun X0 : DiagramMap D (diagram_const X) =>
   (fun
      (DiagramMap_obj : 
       forall i : G, 
       D i -> diagram_const X i)
      (w : forall (i j : G) 
           (g : G i j) 
           (x : D i),
           ((diagram_const X) _f g)
             (DiagramMap_obj i x) =
           DiagramMap_obj j ((D _f g) x)) =>
    {|
      legs := ?legs;
      legs_comm :=
        fun (x y : G) (z : G x y) =>
        (fun z' : D x => (?Goal x y z z')^)
        :
        (fun x0 : D x => ?legs y ((D _f z) x0)) ==
        ?legs x
    |}) X0 (DiagramMap_comm X0)) == idmap
    1,2: exact w.
G: Graph
H: Funext
D: Diagram G
X: Type
(fun X0 : DiagramMap D (diagram_const X) =>
 (fun
    (DiagramMap_obj : forall i : G,
                      D i -> diagram_const X i)
    (w : forall (i j : G) (g : G i j) (x : D i),
         ((diagram_const X) _f g) (DiagramMap_obj i x) =
         DiagramMap_obj j ((D _f g) x)) =>
  {|
    legs := DiagramMap_obj;
    legs_comm :=
      fun (x y : G) (z : G x y) =>
      (fun z' : D x => (w x y z z')^)
      :
      (fun x0 : D x => DiagramMap_obj y ((D _f z) x0)) ==
      DiagramMap_obj x
  |}) X0 (DiagramMap_comm X0))
o (fun X0 : Cocone D X =>
   (fun (legs : forall i : G, D i -> X)
      (w : forall (i j : G) (g : G i j),
           (fun x : D i => legs j ((D _f g) x)) ==
           legs i) =>
    {|
      DiagramMap_obj := legs;
      DiagramMap_comm :=
        fun (x y : G) (z : G x y) (z' : D x) =>
        (w x y z z')^
    |}) X0 (legs_comm X0)) == idmap
G: Graph
H: Funext
D: Diagram G
X: Type
(fun X0 : Cocone D X =>
 (fun (legs : forall i : G, D i -> X)
    (w : forall (i j : G) (g : G i j),
         (fun x : D i => legs j ((D _f g) x)) ==
         legs i) =>
  {|
    DiagramMap_obj := legs;
    DiagramMap_comm :=
      fun (x y : G) (z : G x y) (z' : D x) =>
      (w x y z z')^
  |}) X0 (legs_comm X0))
o (fun X0 : DiagramMap D (diagram_const X) =>
   (fun
      (DiagramMap_obj : forall i : G,
                        D i -> diagram_const X i)
      (w : forall (i j : G) (g : G i j) (x : D i),
           ((diagram_const X) _f g)
             (DiagramMap_obj i x) =
           DiagramMap_obj j ((D _f g) x)) =>
    {|
      legs := DiagramMap_obj;
      legs_comm :=
        fun (x y : G) (z : G x y) =>
        (fun z' : D x => (w x y z z')^)
        :
        (fun x0 : D x =>
         DiagramMap_obj y ((D _f z) x0)) ==
        DiagramMap_obj x
    |}) X0 (DiagramMap_comm X0)) == idmap
    1,2: intros[].
G: Graph
H: Funext
D: Diagram G
X: Type
legs: forall i : G, D i -> X
legs_comm: forall (i j : G) (g : G i j),
(fun x : D i => legs j ((D _f g) x)) ==
legs i
{|
  legs := legs;
  legs_comm :=
    fun (x y : G) (z : G x y) (z' : D x) =>
    ((legs_comm x y z z')^)^
|} = {| legs := legs; legs_comm := legs_comm |}
G: Graph
H: Funext
D: Diagram G
X: Type
DiagramMap_obj: forall i : G,
D i -> diagram_const X i
DiagramMap_comm: forall (i j : G) (g : G i j)
(x : D i),
((diagram_const X) _f g)
  (DiagramMap_obj i x) =
DiagramMap_obj j ((D _f g) x)
{|
  DiagramMap_obj := DiagramMap_obj;
  DiagramMap_comm :=
    fun (x y : G) (z : G x y) (z' : D x) =>
    ((DiagramMap_comm x y z z')^)^
|} =
{|
  DiagramMap_obj := DiagramMap_obj;
  DiagramMap_comm := DiagramMap_comm
|}
    1: srapply path_cocone.
G: Graph
H: Funext
D: Diagram G
X: Type
legs: forall i : G, D i -> X
legs_comm: forall (i j : G) (g : G i j),
(fun x : D i => legs j ((D _f g) x)) ==
legs i
forall i : G,
{|
  legs := legs;
  legs_comm :=
    fun (x y : G) (z : G x y) (z' : D x) =>
    ((legs_comm x y z z')^)^
|} i == {| legs := legs; legs_comm := legs_comm |} i
G: Graph
H: Funext
D: Diagram G
X: Type
legs: forall i : G, D i -> X
legs_comm: forall (i j : G) (g : G i j),
(fun x : D i => legs j ((D _f g) x)) ==
legs i
forall (i j : G) (g : G i j) 
(x : D i),
Cocone.legs_comm
  {|
    legs := legs;
    legs_comm :=
      fun (x0 y : G) (z : G x0 y) (z' : D x0) =>
      ((legs_comm x0 y z z')^)^
  |} i j g x @ ?path_legs i x =
?path_legs j ((D _f g) x) @
Cocone.legs_comm
  {| legs := legs; legs_comm := legs_comm |} i j g x
G: Graph
H: Funext
D: Diagram G
X: Type
DiagramMap_obj: forall i : G,
D i -> diagram_const X i
DiagramMap_comm: forall (i j : G) (g : G i j)
(x : D i),
((diagram_const X) _f g)
  (DiagramMap_obj i x) =
DiagramMap_obj j ((D _f g) x)
{|
  DiagramMap_obj := DiagramMap_obj;
  DiagramMap_comm :=
    fun (x y : G) (z : G x y) (z' : D x) =>
    ((DiagramMap_comm x y z z')^)^
|} =
{|
  DiagramMap_obj := DiagramMap_obj;
  DiagramMap_comm := DiagramMap_comm
|}
    3: srapply path_DiagramMap.
G: Graph
H: Funext
D: Diagram G
X: Type
legs: forall i : G, D i -> X
legs_comm: forall (i j : G) (g : G i j),
(fun x : D i => legs j ((D _f g) x)) ==
legs i
forall i : G,
{|
  legs := legs;
  legs_comm :=
    fun (x y : G) (z : G x y) (z' : D x) =>
    ((legs_comm x y z z')^)^
|} i == {| legs := legs; legs_comm := legs_comm |} i
G: Graph
H: Funext
D: Diagram G
X: Type
legs: forall i : G, D i -> X
legs_comm: forall (i j : G) (g : G i j),
(fun x : D i => legs j ((D _f g) x)) ==
legs i
forall (i j : G) (g : G i j) 
(x : D i),
Cocone.legs_comm
  {|
    legs := legs;
    legs_comm :=
      fun (x0 y : G) (z : G x0 y) (z' : D x0) =>
      ((legs_comm x0 y z z')^)^
  |} i j g x @ ?path_legs i x =
?path_legs j ((D _f g) x) @
Cocone.legs_comm
  {| legs := legs; legs_comm := legs_comm |} i j g x
G: Graph
H: Funext
D: Diagram G
X: Type
DiagramMap_obj: forall i : G,
D i -> diagram_const X i
DiagramMap_comm: forall (i j : G) (g : G i j)
(x : D i),
((diagram_const X) _f g)
  (DiagramMap_obj i x) =
DiagramMap_obj j ((D _f g) x)
forall i : G,
{|
  DiagramMap_obj := DiagramMap_obj;
  DiagramMap_comm :=
    fun (x y : G) (z : G x y) (z' : D x) =>
    ((DiagramMap_comm x y z z')^)^
|} i ==
{|
  DiagramMap_obj := DiagramMap_obj;
  DiagramMap_comm := DiagramMap_comm
|} i
G: Graph
H: Funext
D: Diagram G
X: Type
DiagramMap_obj: forall i : G,
D i -> diagram_const X i
DiagramMap_comm: forall (i j : G) (g : G i j)
(x : D i),
((diagram_const X) _f g)
  (DiagramMap_obj i x) =
DiagramMap_obj j ((D _f g) x)
forall (i j : G) (g : G i j) 
(x : D i),
Diagram.DiagramMap_comm
  {|
    DiagramMap_obj := DiagramMap_obj;
    DiagramMap_comm :=
      fun (x0 y : G) (z : G x0 y) (z' : D x0) =>
      ((DiagramMap_comm x0 y z z')^)^
  |} g x @ ?h_obj j ((D _f g) x) =
ap ((diagram_const X) _f g) (?h_obj i x) @
Diagram.DiagramMap_comm
  {|
    DiagramMap_obj := DiagramMap_obj;
    DiagramMap_comm := DiagramMap_comm
  |} g x
    1,3: reflexivity.
G: Graph
H: Funext
D: Diagram G
X: Type
legs: forall i : G, D i -> X
legs_comm: forall (i j : G) (g : G i j),
(fun x : D i => legs j ((D _f g) x)) ==
legs i
forall (i j : G) (g : G i j) (x : D i),
Cocone.legs_comm
  {|
    legs := legs;
    legs_comm :=
      fun (x0 y : G) (z : G x0 y) (z' : D x0) =>
      ((legs_comm x0 y z z')^)^
  |} i j g x @ (fun (i0 : G) (x0 : D i0) => 1) i x =
(fun (i0 : G) (x0 : D i0) => 1) j ((D _f g) x) @
Cocone.legs_comm
  {| legs := legs; legs_comm := legs_comm |} i j g x
G: Graph
H: Funext
D: Diagram G
X: Type
DiagramMap_obj: forall i : G,
D i -> diagram_const X i
DiagramMap_comm: forall (i j : G) (g : G i j)
(x : D i),
((diagram_const X) _f g)
  (DiagramMap_obj i x) =
DiagramMap_obj j ((D _f g) x)
forall (i j : G) (g : G i j) 
(x : D i),
Diagram.DiagramMap_comm
  {|
    DiagramMap_obj := DiagramMap_obj;
    DiagramMap_comm :=
      fun (x0 y : G) (z : G x0 y) (z' : D x0) =>
      ((DiagramMap_comm x0 y z z')^)^
  |} g x @
(fun (i0 : G) (x0 : D i0) => 1) j ((D _f g) x) =
ap ((diagram_const X) _f g)
  ((fun (i0 : G) (x0 : D i0) => 1) i x) @
Diagram.DiagramMap_comm
  {|
    DiagramMap_obj := DiagramMap_obj;
    DiagramMap_comm := DiagramMap_comm
  |} g x
    all: cbn; intros; hott_simpl.
  Defined.

  Definition equiv_diagram_const_cone `{Funext} (X : Type) (D : Diagram G)
    : DiagramMap (diagram_const X) D <~> Cone X D.
G: Graph
H: Funext
X: Type
D: Diagram G
DiagramMap (diagram_const X) D <~> Cone X D
  Proof.
G: Graph
H: Funext
X: Type
D: Diagram G
DiagramMap (diagram_const X) D <~> Cone X D
    srapply equiv_adjointify.
G: Graph
H: Funext
X: Type
D: Diagram G
DiagramMap (diagram_const X) D -> Cone X D
G: Graph
H: Funext
X: Type
D: Diagram G
Cone X D -> DiagramMap (diagram_const X) D
G: Graph
H: Funext
X: Type
D: Diagram G
?f o ?g == idmap
G: Graph
H: Funext
X: Type
D: Diagram G
?g o ?f == idmap
    1,2: intros [? w]; econstructor.
G: Graph
H: Funext
X: Type
D: Diagram G
DiagramMap_obj: forall i : G,
diagram_const X i -> D i
w: forall (i j : G) (g : G i j)
(x : diagram_const X i),
(D _f g) (DiagramMap_obj i x) =
DiagramMap_obj j (((diagram_const X) _f g) x)
forall (i j : G) (g : G i j),
(fun x : X => (D _f g) (?legs i x)) == ?legs j
G: Graph
H: Funext
X: Type
D: Diagram G
legs: forall i : G, X -> D i
w: forall (i j : G) (g : G i j),
(fun x : X => (D _f g) (legs i x)) == legs j
forall (i j : G) (g : G i j) 
(x : diagram_const X i),
(D _f g) (?DiagramMap_obj i x) =
?DiagramMap_obj j (((diagram_const X) _f g) x)
G: Graph
H: Funext
X: Type
D: Diagram G
(fun X0 : DiagramMap (diagram_const X) D =>
 (fun
    (DiagramMap_obj : 
     forall i : G, diagram_const X i -> D i)
    (w : forall (i j : G) 
         (g : G i j) 
         (x : diagram_const X i),
         (D _f g) (DiagramMap_obj i x) =
         DiagramMap_obj j (((diagram_const X) _f g) x))
  => {| Cone.legs := ?legs; Cone.legs_comm := ?Goal |})
   X0 (DiagramMap_comm X0))
o (fun X0 : Cone X D =>
   (fun (legs : forall i : G, X -> D i)
      (w : forall (i j : G) 
           (g : G i j),
           (fun x : X => (D _f g) (legs i x)) ==
           legs j) =>
    {|
      DiagramMap_obj := ?DiagramMap_obj;
      DiagramMap_comm := ?Goal0
    |}) X0 (Cone.legs_comm X0)) == idmap
G: Graph
H: Funext
X: Type
D: Diagram G
(fun X0 : Cone X D =>
 (fun (legs : forall i : G, X -> D i)
    (w : forall (i j : G) 
         (g : G i j),
         (fun x : X => (D _f g) (legs i x)) == legs j)
  =>
  {|
    DiagramMap_obj := ?DiagramMap_obj;
    DiagramMap_comm := ?Goal0
  |}) X0 (Cone.legs_comm X0))
o (fun X0 : DiagramMap (diagram_const X) D =>
   (fun
      (DiagramMap_obj : 
       forall i : G, 
       diagram_const X i -> D i)
      (w : forall (i j : G) 
           (g : G i j) 
           (x : diagram_const X i),
           (D _f g) (DiagramMap_obj i x) =
           DiagramMap_obj j
             (((diagram_const X) _f g) x)) =>
    {| Cone.legs := ?legs; Cone.legs_comm := ?Goal |})
     X0 (DiagramMap_comm X0)) == idmap
    1,2: exact w.
G: Graph
H: Funext
X: Type
D: Diagram G
(fun X0 : DiagramMap (diagram_const X) D =>
 (fun
    (DiagramMap_obj : forall i : G,
                      diagram_const X i -> D i)
    (w : forall (i j : G) (g : G i j)
         (x : diagram_const X i),
         (D _f g) (DiagramMap_obj i x) =
         DiagramMap_obj j (((diagram_const X) _f g) x))
  =>
  {|
    Cone.legs := DiagramMap_obj; Cone.legs_comm := w
  |}) X0 (DiagramMap_comm X0))
o (fun X0 : Cone X D =>
   (fun (legs : forall i : G, X -> D i)
      (w : forall (i j : G) (g : G i j),
           (fun x : X => (D _f g) (legs i x)) ==
           legs j) =>
    {| DiagramMap_obj := legs; DiagramMap_comm := w |})
     X0 (Cone.legs_comm X0)) == idmap
G: Graph
H: Funext
X: Type
D: Diagram G
(fun X0 : Cone X D =>
 (fun (legs : forall i : G, X -> D i)
    (w : forall (i j : G) (g : G i j),
         (fun x : X => (D _f g) (legs i x)) == legs j)
  =>
  {| DiagramMap_obj := legs; DiagramMap_comm := w |})
   X0 (Cone.legs_comm X0))
o (fun X0 : DiagramMap (diagram_const X) D =>
   (fun
      (DiagramMap_obj : forall i : G,
                        diagram_const X i -> D i)
      (w : forall (i j : G) (g : G i j)
           (x : diagram_const X i),
           (D _f g) (DiagramMap_obj i x) =
           DiagramMap_obj j
             (((diagram_const X) _f g) x)) =>
    {|
      Cone.legs := DiagramMap_obj; Cone.legs_comm := w
    |}) X0 (DiagramMap_comm X0)) == idmap
    1,2: intros[].
G: Graph
H: Funext
X: Type
D: Diagram G
legs: forall i : G, X -> D i
legs_comm: forall (i j : G) (g : G i j),
(fun x : X => (D _f g) (legs i x)) ==
legs j
{| Cone.legs := legs; Cone.legs_comm := legs_comm |} =
{| Cone.legs := legs; Cone.legs_comm := legs_comm |}
G: Graph
H: Funext
X: Type
D: Diagram G
DiagramMap_obj: forall i : G,
diagram_const X i -> D i
DiagramMap_comm: forall (i j : G) (g : G i j)
(x : diagram_const X i),
(D _f g) (DiagramMap_obj i x) =
DiagramMap_obj j
  (((diagram_const X) _f g) x)
{|
  DiagramMap_obj := DiagramMap_obj;
  DiagramMap_comm := DiagramMap_comm
|} =
{|
  DiagramMap_obj := DiagramMap_obj;
  DiagramMap_comm := DiagramMap_comm
|}
    1: srapply path_cone.
G: Graph
H: Funext
X: Type
D: Diagram G
legs: forall i : G, X -> D i
legs_comm: forall (i j : G) (g : G i j),
(fun x : X => (D _f g) (legs i x)) ==
legs j
forall i : G,
{| Cone.legs := legs; Cone.legs_comm := legs_comm |} i ==
{| Cone.legs := legs; Cone.legs_comm := legs_comm |} i
G: Graph
H: Funext
X: Type
D: Diagram G
legs: forall i : G, X -> D i
legs_comm: forall (i j : G) (g : G i j),
(fun x : X => (D _f g) (legs i x)) ==
legs j
forall (i j : G) (g : G i j) 
(x : X),
Cone.legs_comm
  {| Cone.legs := legs; Cone.legs_comm := legs_comm |}
  i j g x @ ?path_legs j x =
ap (D _f g) (?path_legs i x) @
Cone.legs_comm
  {| Cone.legs := legs; Cone.legs_comm := legs_comm |}
  i j g x
G: Graph
H: Funext
X: Type
D: Diagram G
DiagramMap_obj: forall i : G,
diagram_const X i -> D i
DiagramMap_comm: forall (i j : G) (g : G i j)
(x : diagram_const X i),
(D _f g) (DiagramMap_obj i x) =
DiagramMap_obj j
  (((diagram_const X) _f g) x)
{|
  DiagramMap_obj := DiagramMap_obj;
  DiagramMap_comm := DiagramMap_comm
|} =
{|
  DiagramMap_obj := DiagramMap_obj;
  DiagramMap_comm := DiagramMap_comm
|}
    3: srapply path_DiagramMap.
G: Graph
H: Funext
X: Type
D: Diagram G
legs: forall i : G, X -> D i
legs_comm: forall (i j : G) (g : G i j),
(fun x : X => (D _f g) (legs i x)) ==
legs j
forall i : G,
{| Cone.legs := legs; Cone.legs_comm := legs_comm |} i ==
{| Cone.legs := legs; Cone.legs_comm := legs_comm |} i
G: Graph
H: Funext
X: Type
D: Diagram G
legs: forall i : G, X -> D i
legs_comm: forall (i j : G) (g : G i j),
(fun x : X => (D _f g) (legs i x)) ==
legs j
forall (i j : G) (g : G i j) 
(x : X),
Cone.legs_comm
  {| Cone.legs := legs; Cone.legs_comm := legs_comm |}
  i j g x @ ?path_legs j x =
ap (D _f g) (?path_legs i x) @
Cone.legs_comm
  {| Cone.legs := legs; Cone.legs_comm := legs_comm |}
  i j g x
G: Graph
H: Funext
X: Type
D: Diagram G
DiagramMap_obj: forall i : G,
diagram_const X i -> D i
DiagramMap_comm: forall (i j : G) (g : G i j)
(x : diagram_const X i),
(D _f g) (DiagramMap_obj i x) =
DiagramMap_obj j
  (((diagram_const X) _f g) x)
forall i : G,
{|
  DiagramMap_obj := DiagramMap_obj;
  DiagramMap_comm := DiagramMap_comm
|} i ==
{|
  DiagramMap_obj := DiagramMap_obj;
  DiagramMap_comm := DiagramMap_comm
|} i
G: Graph
H: Funext
X: Type
D: Diagram G
DiagramMap_obj: forall i : G,
diagram_const X i -> D i
DiagramMap_comm: forall (i j : G) (g : G i j)
(x : diagram_const X i),
(D _f g) (DiagramMap_obj i x) =
DiagramMap_obj j
  (((diagram_const X) _f g) x)
forall (i j : G) (g : G i j) 
(x : diagram_const X i),
Diagram.DiagramMap_comm
  {|
    DiagramMap_obj := DiagramMap_obj;
    DiagramMap_comm := DiagramMap_comm
  |} g x @ ?h_obj j (((diagram_const X) _f g) x) =
ap (D _f g) (?h_obj i x) @
Diagram.DiagramMap_comm
  {|
    DiagramMap_obj := DiagramMap_obj;
    DiagramMap_comm := DiagramMap_comm
  |} g x
    1,3: reflexivity.
G: Graph
H: Funext
X: Type
D: Diagram G
legs: forall i : G, X -> D i
legs_comm: forall (i j : G) (g : G i j),
(fun x : X => (D _f g) (legs i x)) ==
legs j
forall (i j : G) (g : G i j) (x : X),
Cone.legs_comm
  {| Cone.legs := legs; Cone.legs_comm := legs_comm |}
  i j g x @ (fun (i0 : G) (x0 : X) => 1) j x =
ap (D _f g) ((fun (i0 : G) (x0 : X) => 1) i x) @
Cone.legs_comm
  {| Cone.legs := legs; Cone.legs_comm := legs_comm |}
  i j g x
G: Graph
H: Funext
X: Type
D: Diagram G
DiagramMap_obj: forall i : G,
diagram_const X i -> D i
DiagramMap_comm: forall (i j : G) (g : G i j)
(x : diagram_const X i),
(D _f g) (DiagramMap_obj i x) =
DiagramMap_obj j
  (((diagram_const X) _f g) x)
forall (i j : G) (g : G i j) 
(x : diagram_const X i),
Diagram.DiagramMap_comm
  {|
    DiagramMap_obj := DiagramMap_obj;
    DiagramMap_comm := DiagramMap_comm
  |} g x @
(fun (i0 : G) (x0 : X) => 1) j
  (((diagram_const X) _f g) x) =
ap (D _f g) ((fun (i0 : G) (x0 : X) => 1) i x) @
Diagram.DiagramMap_comm
  {|
    DiagramMap_obj := DiagramMap_obj;
    DiagramMap_comm := DiagramMap_comm
  |} g x
    all: cbn; intros; hott_simpl.
  Defined.

End ConstantDiagram.