proposition: Lemma is_omega_cont_functor_into_product_category {F : functor A (product_category B)} (HF : ∏ (i : I), is_omega_cont (functor_composite F (pr_functor I B i))) : is_omega_cont F.
proof: Proof. intros cA a cc Hcc. apply isLimCone_in_product_category. intros i. rewrite <- mapcone_functor_composite. now apply HF, Hcc. Defined.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.Slice UniMath.CategoryTheory.Categories.HSET.Limits UniMath.CategoryTheory.Categories.HSET.Limits UniMath.CategoryTheory.Categories.HSET.Structures UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Limits.Initial UniMath.CategoryTheory.FunctorAlgebras UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Products UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.ProductCategory UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Adjunctions.Examples UniMath.CategoryTheory.exponentials UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.RightKanExtension UniMath.CategoryTheory.slicecat UniMath.CategoryTheory.Chains.Chains UniMath.CategoryTheory.Chains.Cochains UniMath.CategoryTheory.OppositeCategory.Core UniMath.CategoryTheory.OppositeCategory.LimitsAsColimits UniMath.CategoryTheory.OppositeCategory.OppositeOfFunctorCategory UniMath.CategoryTheory.Chains.OmegaCocontFunctors UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.Equivalences.CompositesAndInverses