Definition eq_diag {C : category} {g : graph} (d d' : diagram g C) := ∑ (eq_v : ∏ v: vertex g, dob d v = dob d' v), ∏ (v v':vertex g) (f:edge v v'), transportf (λ obj, C⟦obj, dob d v'⟧) (eq_v v) (dmor d f) = transportb (λ obj, C⟦_, obj⟧) (eq_v v') (dmor d' f).
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.