proposition: Lemma is_omega_cont_pre_composition_functor' {A B C : category} (F : functor A B) (H : Lims_of_shape conat_graph C) : is_omega_cont (pre_composition_functor _ _ C F).
proof: Proof. use (is_omega_cocont_op (F := functor_op (pre_composition_functor _ _ C F))). use is_omega_cocont_z_iso. 2: { set (facto := functor_op_of_precomp_functor_factorizes_through_functorcatofopp_nat_z_iso C F). set (t := z_iso_inv (z_iso_from_nat_z_iso (homset_property _) facto)). exact t. } repeat (use is_omega_cocont_functor_composite). 2: { apply is_omega_cocont_pre_composition_functor. intro ch. repeat (use tpair). - exact (pr1 (pr1 (H (chain_op ch)))). - exact (λ v, pr1 (pr2 (pr1 (H (chain_op ch)))) v). - exact (λ u v e, pr2 (pr2 (pr1 (H (chain_op ch)))) v u e). - exact (λ c cc, ((pr2 (H (chain_op ch))) c (cocone_op cc))). } - use is_cocont_equivalence_of_cats. exact (adj_equivalence_of_cats_inv (opfunctorcat_adjequiv_functorcatofoppcats B C)). - use is_cocont_equivalence_of_cats. apply opfunctorcat_adjequiv_functorcatofoppcats. 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