{C1 C2 : Cone X D} (P := fun q' => forall (i j : G) (g : G i j) (x : X), D _f g (q' i x) = q' j x) (path_legs : legs C1 = legs C2) (path_legs_comm : transport P path_legs (legs_comm C1) = legs_comm C2) : C1 = C2 := match path_legs_comm in (_ = v1) return C1 = {|legs := legs C2; legs_comm := v1 |} with | idpath => match path_legs in (_ = v0) return C1 = {|legs := v0; legs_comm := path_legs # (legs_comm C1) |} with | idpath => 1 end end.
Require Import Basics. Require Import Types. Require Import Diagrams.Graph. Require Import Diagrams.Diagram.