Definition iscolimcocone_chain_op {C : category} {g : chain C} {c : C} {cc : cocone g c} (cc_lim : isColimCocone g c cc) : isLimCone (chain_op g) c (cocone_op cc). Proof. apply (iscolimcocone_op cc_lim). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.OppositeCategory.Core. Require Import UniMath.CategoryTheory.Limits.Cones. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Chains.Chains. Require Import UniMath.CategoryTheory.Chains.Cochains.