proposition: Lemma post_comp_with_pr_and_hat_is_omega_cont (s t : sort) : is_omega_cont (post_comp_functor (A := sortToC) (projSortToC sort Hsort C s ∙ hat_functor sort Hsort C CC t) ).
proof: Proof. intros coch L con isLimcon. apply Limits.pointwise_Lim_is_isLimFunctor ; intro F. apply Limits.pointwise_Lim_is_isLimFunctor ; intro G. use Limits.is_z_iso_isLim. { apply LC. } transparent assert (x : (t = G → cochain C)). { intro p. use tpair. - intro n. exact (pr1 (pr1 (dob coch n) F) s). - intros n m q. exact (pr1 (pr1 (dmor coch q) F) s). } use make_is_z_isomorphism. - refine (pr1 (distr (_,,Hsort t G) x) · _). assert (bla : (∏ a : sortToC, LimCone (diagram_pointwise coch a))). { intro ; apply ω_complete_functor_cat ; exact LC. } assert (bla' : (∏ a : path_pregroupoid sort Hsort, LimCone (diagram_pointwise (diagram_pointwise coch F) a))). { intro ; apply LC. } set (LF_lim := Limits.isLimFunctor_is_pointwise_Lim coch bla _ _ isLimcon F). set (LFs_lim := Limits.isLimFunctor_is_pointwise_Lim _ bla' _ _ LF_lim s). set (LFs_cone := make_LimCone _ _ _ LFs_lim). use CoproductOfArrows. intro i. exact (pr1 (z_iso_inv (z_iso_from_lim_to_lim LFs_cone (LC (x i))))). - split. + etrans. 1: apply assoc. use (z_iso_inv_to_right _ _ _ _ (_ ,, CoproductOfArrowsIsos _ _ _ _ _ _ _ _: z_iso _ _)). { intro ; apply (pr2 (z_iso_inv _)). } rewrite ! id_left. use (z_iso_inv_to_right _ _ _ _ (z_iso_inv (make_z_iso _ _ (pr2 (distr _ _))))). apply pathsinv0, limArrowUnique. intro n. rewrite assoc'. etrans. 1: { apply maponpaths. apply limArrowCommutes. } etrans. 1: { apply precompWithCoproductArrow. } cbn. unfold CoproductOfArrows. apply maponpaths. apply funextsec ; intro p. rewrite ! assoc. apply maponpaths_2. apply (Graphs.Limits.limArrowCommutes (LC (x p))). + etrans. 1: apply assoc'. apply pathsinv0. transparent assert (d_i : (is_z_isomorphism ( pr1 (distr ((t = G),, Hsort t G) x)))). { exists (coproduct_of_limit_to_limit_of_coproduct C LC (CC (t = G) (Hsort t G)) x). set (q := distr ((t = G),, Hsort t G) x). split ; apply (pr2 q). } use (z_iso_inv_to_left _ _ _ (_,,d_i)). refine (id_right _ @ _). use (z_iso_inv_to_left _ _ _ (CoproductOfArrows _ _ _ _ _,, _ : z_iso _ _)). { use CoproductOfArrowsIsos ; intro. apply is_z_iso_inv_from_z_iso. } apply limArrowUnique. intro n. etrans. 1: apply assoc'. etrans. 1: { apply maponpaths. apply (limArrowCommutes (LC (diagram_pointwise (diagram_pointwise (mapdiagram (post_comp_functor (projSortToC sort Hsort C s ∙ hat_functor sort Hsort C CC t)) coch) F) G))). } etrans. 1: { apply precompWithCoproductArrow. } cbn. unfold CoproductOfArrows. apply maponpaths. apply funextsec ; intro p. rewrite ! assoc. apply maponpaths_2. apply (Graphs.Limits.limArrowCommutes (LC (x p))). Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.Lists UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Products UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.Initial UniMath.CategoryTheory.FunctorAlgebras UniMath.CategoryTheory.exponentials UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Chains.All UniMath.CategoryTheory.Monads.Monads UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.Limits UniMath.CategoryTheory.Categories.HSET.Colimits UniMath.CategoryTheory.Categories.HSET.Structures UniMath.CategoryTheory.Categories.StandardCategories UniMath.CategoryTheory.Groupoids UniMath.SubstitutionSystems.Signatures UniMath.SubstitutionSystems.SumOfSignatures UniMath.SubstitutionSystems.BinProductOfSignatures UniMath.SubstitutionSystems.MultiSorted_alt UniMath.CategoryTheory.Chains.OmegaContFunctors UniMath.SubstitutionSystems.ContinuitySignature.GeneralLemmas UniMath.SubstitutionSystems.ContinuitySignature.CommutingOfOmegaLimitsAndCoproducts