Lemma eq_is_eq_diag {C : category} {g : graph} (d d' : diagram g C) : d = d' -> eq_diag d d'. Proof. intro e. induction e. exists (λ x, idpath _). exact (λ x y z, idpath _). Qed.
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.