proposition: Lemma eq_is_eq_diag {C : category} {g : graph} (d d' : diagram g C) : d = d' -> eq_diag d d'.
proof: Proof. intro e. induction e. exists (λ x, idpath _). exact (λ x y z, idpath _). Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.TransportMorphisms UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Graphs.Limits