proposition: Lemma Ff_right_tensor_preserves_colimit_mor : (monoidal_right_tensor A) (colim (FfCC d)) --> colim (FfCC (mapdiagram (monoidal_right_tensor A) d)).
proof: Proof. use tpair. - intro f. exists (Ff_right_tensor_preserves_colimit_mor11 f). abstract ( split; [ etrans; [apply assoc'|]; apply pathsinv0; etrans; [apply id_left|]; etrans; [apply assoc'|]; apply cancel_precomposition; apply pathsinv0; etrans; [apply assoc'|]; apply cancel_precomposition; apply (colimArrowCommutes (CCFf_pt_ob1 CC d (fact_R A f))) | etrans; [apply id_right|]; apply pathsinv0; use colimArrowUnique; intro v; etrans; [apply assoc|]; etrans; [apply cancel_postcomposition; apply (colimArrowCommutes (CCFf_pt_ob1 CC d (fact_R A f)))|]; apply (colimArrowCommutes (CCFf_pt_ob1 CC (mapdiagram (monoidal_right_tensor A) d) f)) ] ). - abstract ( intros f f' γ; apply subtypePath; [intro; apply isapropdirprod; apply homset_property|]; etrans; [use pr1_transportf_const|]; etrans; [apply precompWithColimOfArrows|]; apply pathsinv0; etrans; [apply postcompWithColimArrow|]; apply maponpaths; use cocone_paths; intro v; etrans; [use (colimOfArrowsIn _ _ (CCFf_pt_ob1 CC (mapdiagram (monoidal_right_tensor A) d) f) _ _ _ v)|]; reflexivity ). 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