Definition is_omega_cont_op {C D : category} {F : functor C D} (oc : is_omega_cont F) : is_omega_cocont (functor_op F). Proof. intros ch c cc. set (t := oc (chain_op ch) c (cocone_op cc)). intro col. set (tt := iscolimcocone_chain_op col). intros c0 cc0. apply (t tt c0 (cocone_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.