Definition LimCone_op {C : category} {g : graph} {d : diagram g C} (cc : LimCone d) : ColimCocone (diagram_op d). Proof. exists (pr1 (pr1 cc) ,, cone_op (pr2 (pr1 cc))). exact (islimcone_op (pr2 cc)). 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.