proposition: Lemma monoidal_right_tensor_cocone {C : category} (V : monoidal C) (A : C) {g : graph} (d : diagram g _) (CC : ColimCocone d) (CMon := (C,, V) : monoidal_cat) : cocone (mapdiagram (monoidal_right_tensor (A : CMon)) d) (monoidal_right_tensor (A : CMon) (colim CC)).
proof: Proof. use tpair. - intro v. exact (colimIn _ v ⊗^{V}_{r} A). - abstract ( intros u v e; etrans; [apply maponpaths_2|]; [ etrans; [apply cancel_precomposition; apply (bifunctor_leftid V)|]; apply (id_right (dmor d e ⊗^{V}_{r} A)) |]; etrans; [apply (pathsinv0 (bifunctor_rightcomp V _ _ _ _ _ _))|]; apply maponpaths; apply (colimInCommutes _ _ _ e) ). 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