Lemma post_comp_with_pr_and_hat_is_omega_cont (s t : sort) : is_omega_cont (post_comp_functor (A := sortToC) (projSortToC s ∙ hat_functorC t) ). 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 s ∙ hat_functorC 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.Combinatorics.Lists. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. 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.Initial. Require Import UniMath.CategoryTheory.FunctorAlgebras. Require Import UniMath.CategoryTheory.exponentials. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Chains.All. Require Import UniMath.CategoryTheory.Monads.Monads. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Categories.HSET.Limits. Require Import UniMath.CategoryTheory.Categories.HSET.Colimits. Require Import UniMath.CategoryTheory.Categories.HSET.Structures. Require Import UniMath.CategoryTheory.Categories.StandardCategories. Require Import UniMath.CategoryTheory.Groupoids. Require Import UniMath.SubstitutionSystems.Signatures. Require Import UniMath.SubstitutionSystems.SumOfSignatures. Require Import UniMath.SubstitutionSystems.BinProductOfSignatures. Require Import UniMath.SubstitutionSystems.MultiSortedBindingSig. Require Import UniMath.SubstitutionSystems.MultiSorted_alt. Require Import UniMath.CategoryTheory.Chains.OmegaContFunctors. Require Import UniMath.SubstitutionSystems.ContinuitySignature.GeneralLemmas. Require Import UniMath.SubstitutionSystems.ContinuitySignature.CommutingOfOmegaLimitsAndCoproducts.