Lemma make_eq_diag_cocone : ∏ {C : category} {g : graph} {d : diagram g C} (d' : diagram g C) (heq_d: eq_diag d d') {c : C} (cc:cocone d c), cocone d' c. Proof. clear. intros. destruct heq_d as [heq heq2]. use make_cocone. intro v. use (transportf (λ obj, C⟦obj,_⟧ ) (heq v)); simpl. apply (coconeIn cc). abstract( intros u v e; simpl; rewrite <- ( coconeInCommutes cc u v e); apply (pathscomp0 (b:=transportb (precategory_morphisms (dob d' u)) (heq v) (dmor d' e) · (coconeIn cc v))); [ unfold transportb; (set (z:= ! heq v)); rewrite <- (pathsinv0inv0 (heq v)); apply pathsinv0; apply transport_compose|]; etrans; [ apply cancel_postcomposition; eapply pathsinv0; apply heq2|]; clear; now destruct (heq u)). 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.