Definition is_cocont_op {C D : category} {F : functor C D} (oc : is_cocont F) : is_cont (functor_op F). Proof. intros g d c cc. set (t := oc _ _ c (cone_op cc)). intro lm. set (tt := islimcone_op lm). intros c0 cc0. apply (t tt c0 (cone_op cc0)). 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.