{C1 C2 : Cocone D X} (path_legs : forall i, C1 i == C2 i) (path_legs_comm : forall i j g x, legs_comm C1 i j g x @ path_legs i x = path_legs j (D _f g x) @ legs_comm C2 i j g x) : C1 = C2. Proof. destruct C1 as [legs pp_q], C2 as [r pp_r]. refine (path_cocone_naive (path_forall _ _ (fun i => path_forall _ _ (path_legs i))) _). cbn; funext i j f x. rewrite 4 transport_forall_constant, transport_paths_FlFr. rewrite concat_pp_p; apply moveR_Vp. rewrite 2 (ap_apply_lD2 (path_forall _ _ (fun i => path_forall _ _ (path_legs i)))). rewrite 3 eisretr. apply path_legs_comm. Defined.
Require Import Basics. Require Import Types. Require Import Diagrams.Graph. Require Import Diagrams.Diagram.