Definition is_omega_cont {C D : category} (F : functor C D) : UU := ∏ (c : cochain C) (L : C) (cc : cone c L), preserves_limit F c L cc.
Require Import UniMath.Foundations.PartA. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Terminal.