Lemma make_eq_diag_cone : ∏ {C : category} {g : graph} {d : diagram g C} (d' : diagram g C) (heq_d: eq_diag d d') {c : C} (cc:cone d c), cone d' c. Proof. clear. intros. set (heq := pr1 heq_d). set (heq2 := pr2 heq_d). use make_cone. intro v. apply (transportf (λ obj, C⟦_,obj⟧ ) (heq v) (coneOut cc v)). abstract( intros u v e; simpl; rewrite <- ( coneOutCommutes cc u v e); etrans;[ apply transport_compose|]; rewrite transport_target_postcompose; apply cancel_precomposition; apply transportf_transpose_right; etrans;[ apply (transport_swap (λ a b, C⟦a,b⟧))|]; etrans;[ apply maponpaths; eapply pathsinv0; apply heq2|]; unfold heq; induction (pr1 heq_d u); apply idpath). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.TransportMorphisms. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits.