proposition: Lemma FR_lt_preserves_colim_impl_Ff_lt_preserves_colim (F : Ff C) (d : chain Ff_mon) (CL := ChainsFf CC d) : FR_slice_omega_small F -> isColimCocone _ _ (mapcocone (monoidal_left_tensor (F : Ff_mon)) _ (colimCocone CL)).
proof: Proof. intro HR. set (FfCC := ChainsFf CC (mapdiagram (monoidal_left_tensor (F : Ff_mon)) d)). use (is_z_iso_isColim _ FfCC). exists (FR_lt_preserves_colim_impl_Ff_lt_preserves_colim_mor F d HR). split. - functorial_factorization_mor_eq f. set (HRCC := FR_slice_colimcocone_over_pointwise_tensored F d HR f). set (base_iso := FR_lt_preserves_colim_impl_Ff_lt_preserves_colim_mor_pointwise F d HR f). etrans. apply pr1_transportf_const. apply pathsinv0. etrans. exact (pathsinv0 (pr122 base_iso)). apply compeq; [|reflexivity]. use colimArrowUnique. intro v. etrans. apply colimArrowCommutes. apply pathsinv0. etrans. apply pr1_transportf_const. etrans. apply id_left. apply (section_disp_on_eq_morphisms F); reflexivity. - functorial_factorization_mor_eq f. set (HRCC := FR_slice_colimcocone_over_pointwise_tensored F d HR f). set (base_iso := FR_lt_preserves_colim_impl_Ff_lt_preserves_colim_mor_pointwise F d HR f). etrans. apply pr1_transportf_const. apply pathsinv0. etrans. exact (pathsinv0 (pr222 base_iso)). apply compeq; [reflexivity|]. apply colimArrowUnique. intro v. etrans. apply colimArrowCommutes. apply pathsinv0. etrans. apply pr1_transportf_const. etrans. apply id_left. apply (section_disp_on_eq_morphisms F); reflexivity. 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