proposition: Lemma Ff_lt_preserves_colim_impl_LNWFS_lt_preserves_colim : isColimCocone _ _ (mapcocone (monoidal_left_tensor (pr1 L : Ff_mon)) _ (project_cocone _ _ (colimCocone CL))) -> isColimCocone _ _ (mapcocone (monoidal_left_tensor (L : LNWFS_mon)) _ (colimCocone CL)).
proof: Proof. intro HF. set (HFCC := make_ColimCocone _ _ _ HF). set (base_mor := isColim_is_z_iso _ FfCCbase _ _ HF). set (base_inv := colimArrow FfCCbase _ (colimCocone HFCC)). use (is_z_iso_isColim _ LNWFSCC). use tpair. - exists (pr1 base_mor). abstract ( exact (Ff_lt_preserves_colim_impl_LNWFS_lt_preserves_colim_mor_disp HF) ). - abstract ( apply LNWFS_inv_in_precat_if_Ff_inv_in_precat; exact (Ff_lt_preserves_colim_impl_LNWFS_lt_preserves_colim_inv_in_precat HF) ). Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Pushouts UniMath.CategoryTheory.Limits.Graphs.Coequalizers UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Graphs.EqDiag UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Chains.Chains UniMath.CategoryTheory.slicecat UniMath.CategoryTheory.Monads.Monads UniMath.CategoryTheory.Monads.MonadAlgebras UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.DisplayedCats.Examples.Arrow UniMath.CategoryTheory.DisplayedCats.Examples.Three UniMath.ModelCategories.NWFS UniMath.ModelCategories.Generated.MonoidalHelpers UniMath.ModelCategories.Helpers UniMath.ModelCategories.Generated.LNWFSHelpers UniMath.ModelCategories.Generated.MonoidalHelpers UniMath.ModelCategories.Generated.FFMonoidalStructure UniMath.ModelCategories.Generated.LNWFSMonoidalStructure UniMath.ModelCategories.Generated.LNWFSCocomplete