proposition: Lemma Ff_rt_all_colimits : preserves_colimits_of_shape (monoidal_right_tensor (A : Ff_mon)) g.
proof: Proof. intros d cl cc. intros isCC. set (isCCAcl := Ff_right_tensor_cocone_isColimCocone d). set (CCAcl := ((_,, (monoidal_right_tensor_cocone Ff_mon A d (FfCC d))),, isCCAcl) : ColimCocone _). set (base_iso := isColim_is_z_iso _ (FfCC d) _ _ isCC). use (is_z_iso_isColim _ CCAcl). exists ((pr1 base_iso) ⊗^{_}_{r} A). abstract ( split; [ apply pathsinv0; use colim_endo_is_identity; intro u; etrans; [apply assoc|]; etrans; [apply cancel_postcomposition; apply colimArrowCommutes|]; etrans; [apply cancel_postcomposition, cancel_precomposition; apply (bifunctor_leftid Ff_mon)|]; etrans; [apply cancel_postcomposition, id_right|]; etrans; [exact (pathsinv0 (bifunctor_rightcomp Ff_mon _ _ _ _ _ _))|]; etrans; [apply maponpaths; apply (colimArrowCommutes (make_ColimCocone _ _ _ isCC))|]; reflexivity | apply pathsinv0; etrans; [exact (pathsinv0 (bifunctor_rightid Ff_mon _ _))|]; etrans; [apply maponpaths; exact (pathsinv0 (pr22 base_iso))|]; etrans; [apply (bifunctor_rightcomp Ff_mon)|]; apply cancel_precomposition; use colimArrowUnique; intro u; apply pathsinv0; etrans; [apply cancel_precomposition; apply (bifunctor_leftid Ff_mon)|]; etrans; [apply id_right|]; apply pathsinv0; etrans; [exact (pathsinv0 (bifunctor_rightcomp Ff_mon _ _ _ _ _ _))|]; apply maponpaths; apply colimArrowCommutes ] ). Defined.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Monads.Monads UniMath.CategoryTheory.Monads.MonadAlgebras UniMath.CategoryTheory.Monads.Comonads UniMath.CategoryTheory.Monads.ComonadCoalgebras UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Graphs.Coequalizers UniMath.CategoryTheory.Chains.Chains UniMath.Combinatorics.StandardFiniteSets UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.DisplayedCats.Examples.Arrow UniMath.CategoryTheory.DisplayedCats.Examples.Three UniMath.ModelCategories.NWFS UniMath.ModelCategories.Helpers UniMath.ModelCategories.Generated.MonoidalHelpers UniMath.ModelCategories.Generated.FFMonoidalStructure UniMath.ModelCategories.Generated.LNWFSHelpers UniMath.ModelCategories.Generated.LNWFSMonoidalStructure UniMath.ModelCategories.Generated.LNWFSCocomplete