Require Import Cone. Require Import Cocone. Require Import Diagram. Require Import Diagrams.Graph. (** * Constant diagram *) Section ConstantDiagram. Context {G : Graph}.G: Graph
C: TypeDiagram GG: Graph
C: TypeDiagram GG: Graph
C: TypeG -> TypeG: Graph
C: Typeforall i j : G, G i j -> ?obj i -> ?obj jG: Graph
C: Typeforall i j : G, G i j -> (fun _ : G => C) i -> (fun _ : G => C) jexact idmap. Defined.G: Graph
C: Type
i, j: G
k: G i j(fun _ : G => C) i -> (fun _ : G => C) jG: Graph
A, B: Type
f: A -> BDiagramMap (diagram_const A) (diagram_const B)G: Graph
A, B: Type
f: A -> BDiagramMap (diagram_const A) (diagram_const B)G: Graph
A, B: Type
f: A -> Bforall i : G, diagram_const A i -> diagram_const B iG: Graph
A, B: Type
f: A -> Bforall (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)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) := idpath. Definition diagram_const_functor_idmap {A : Type} : diagram_const_functor (idmap : A -> A) = diagram_idmap (diagram_const A) := idpath.G: Graph
A, B: Type
f: A -> Bforall (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)G: Graph
H: Funext
D: Diagram G
X: TypeDiagramMap D (diagram_const X) <~> Cocone D XG: Graph
H: Funext
D: Diagram G
X: TypeDiagramMap D (diagram_const X) <~> Cocone D X(* The two functions are defined in parallel: *)G: Graph
H: Funext
D: Diagram G
X: TypeDiagramMap D (diagram_const X) -> Cocone D XG: Graph
H: Funext
D: Diagram G
X: TypeCocone D X -> DiagramMap D (diagram_const X)G: Graph
H: Funext
D: Diagram G
X: Type?f o ?g == idmapG: Graph
H: Funext
D: Diagram G
X: Type?g o ?f == idmap(* This reversal is a defect in the definition of [Cocone]. *)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 iG: 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 iforall (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)) == idmapG: 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)) == idmapG: 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 iforall (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)) == idmapG: 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(* The two homotopies are proved in parallel: *)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)) == idmapG: 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)) == idmapG: 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 |}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 iforall i : G, legs i == legs iG: 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 iforall (i j : G) (g : G i j) (x : D i), ((legs_comm i j g x)^)^ @ ?Goal0 i x = ?Goal0 j ((D _f g) x) @ legs_comm i j g xG: 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 |}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 iforall i : G, legs i == legs iG: 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 iforall (i j : G) (g : G i j) (x : D i), ((legs_comm i j g x)^)^ @ ?Goal i x = ?Goal j ((D _f g) x) @ legs_comm i j g xG: 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 i == DiagramMap_obj iG: 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), ((DiagramMap_comm i j g x)^)^ @ ?Goal1 j ((D _f g) x) = ap idmap (?Goal1 i x) @ DiagramMap_comm i j g xG: 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 iforall (i j : G) (g : G i j) (x : D i), ((legs_comm 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) @ legs_comm i j g xG: 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), ((DiagramMap_comm i j g x)^)^ @ (fun (i0 : G) (x0 : D i0) => 1) j ((D _f g) x) = ap idmap ((fun (i0 : G) (x0 : D i0) => 1) i x) @ DiagramMap_comm i j g xG: 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
i, j: G
g: G i j
x: D i((legs_comm i j g x)^)^ @ 1 = 1 @ legs_comm i j g xG: 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)
i, j: G
g: G i j
x: D i((DiagramMap_comm i j g x)^)^ @ 1 = 1 @ DiagramMap_comm i j g x1,2: apply inv_V. Defined.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
i, j: G
g: G i j
x: D i((legs_comm i j g x)^)^ = legs_comm i j g xG: 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)
i, j: G
g: G i j
x: D i((DiagramMap_comm i j g x)^)^ = DiagramMap_comm i j g xG: Graph
H: Funext
X: Type
D: Diagram GDiagramMap (diagram_const X) D <~> Cone X DG: Graph
H: Funext
X: Type
D: Diagram GDiagramMap (diagram_const X) D <~> Cone X DG: Graph
H: Funext
X: Type
D: Diagram GDiagramMap (diagram_const X) D -> Cone X DG: Graph
H: Funext
X: Type
D: Diagram GCone X D -> DiagramMap (diagram_const X) DG: Graph
H: Funext
X: Type
D: Diagram G?f o ?g == idmapG: Graph
H: Funext
X: Type
D: Diagram G?g o ?f == idmapG: 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 jG: 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 jforall (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)) == idmapG: 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)) == idmapG: 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)) == idmapG: 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)) == idmapG: 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 |}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 jforall i : G, {| Cone.legs := legs; Cone.legs_comm := legs_comm |} i == {| Cone.legs := legs; Cone.legs_comm := legs_comm |} iG: 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 jforall (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 xG: 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 |}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 jforall i : G, {| Cone.legs := legs; Cone.legs_comm := legs_comm |} i == {| Cone.legs := legs; Cone.legs_comm := legs_comm |} iG: 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 jforall (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 xG: 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_homotopy {| DiagramMap_obj := DiagramMap_obj; DiagramMap_comm := DiagramMap_comm |} {| DiagramMap_obj := DiagramMap_obj; DiagramMap_comm := DiagramMap_comm |}all: cbn; intros; hott_simpl. Defined. End ConstantDiagram.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 jforall (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