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. 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.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Categories.HSET.Slice. Require Import UniMath.CategoryTheory.Categories.HSET.Limits. Require Import UniMath.CategoryTheory.Categories.HSET.Limits. Require Import UniMath.CategoryTheory.Categories.HSET.Structures. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.FunctorAlgebras. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.ProductCategory. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Adjunctions.Examples. Require Import UniMath.CategoryTheory.exponentials. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.RightKanExtension. Require Import UniMath.CategoryTheory.slicecat. Require Import UniMath.CategoryTheory.Chains.Chains. Require Import UniMath.CategoryTheory.Chains.Cochains. Require Import UniMath.CategoryTheory.OppositeCategory.Core. Require Import UniMath.CategoryTheory.OppositeCategory.LimitsAsColimits. Require Import UniMath.CategoryTheory.OppositeCategory.OppositeOfFunctorCategory. Require Import UniMath.CategoryTheory.Chains.OmegaCocontFunctors. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Equivalences.CompositesAndInverses.