Definition eq_diag_liftcolimcocone {C : category} {g : graph} {d : diagram g C} (d' : diagram g C) (eq_d : eq_diag d d') (cc:ColimCocone d ) : ColimCocone d' := make_ColimCocone _ _ _ (eq_diag_iscolimcocone _ eq_d (isColimCocone_from_ColimCocone cc)).
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.