Definition eq_diag_liftlimcone {C : category} {g : graph} {d : diagram g C} (d' : diagram g C) (eq_d : eq_diag d d') (cc:LimCone d ) : LimCone d' := make_LimCone _ _ _ (eq_diag_islimcone _ eq_d (isLimCone_LimCone 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.