proposition: Lemma Ff_right_tensor_preserves_colimit_mor11 (f : arrow C) : three_ob1 (fact_functor (monoidal_right_tensor A (colim (FfCC d))) f) --> three_ob1 (fact_functor (colim (FfCC (mapdiagram (monoidal_right_tensor A) d))) f).
proof: Proof. use colimArrow. use tpair. - intro v. exact (colimIn (CCFf_pt_ob1 CC (mapdiagram (monoidal_right_tensor A) d) f) v). - abstract ( intros u v e; etrans; [| exact (colimInCommutes ((CCFf_pt_ob1 CC (mapdiagram (monoidal_right_tensor A) d) f)) _ _ e) ]; apply cancel_postcomposition; apply pathsinv0; etrans; [use pr1_transportf_const|]; etrans; [apply cancel_precomposition|]; [ etrans; [use (section_disp_on_eq_morphisms (dob d v) (γ' := identity _)); reflexivity|]; apply maponpaths; apply (section_disp_id (dob d v)) |]; apply id_right ). 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