proposition: Lemma Ff_right_tensor_cocone_isColimCocone : isColimCocone _ _ (monoidal_right_tensor_cocone Ff_mon A d (FfCC d)).
proof: Proof. intros cl cc. set (mor := colimUnivProp (FfCC (mapdiagram (monoidal_right_tensor A) d)) _ cc). destruct mor as [mor uniqueness]. use unique_exists. - apply (compose (Ff_right_tensor_preserves_colimit_mor)). exact (pr1 mor). - abstract ( intro v; etrans; [|exact (pr2 mor v)]; etrans; [apply assoc|]; apply cancel_postcomposition; functorial_factorization_mor_eq f; etrans; [apply pr1_transportf_const|]; apply (colimArrowCommutes (CCFf_pt_ob1 CC d (fact_R A f))) ). - abstract (intro; apply impred; intro; apply homset_property). - abstract ( intros y Hy; apply (pre_comp_with_z_iso_is_inj (z_iso_inv (Ff_right_tensor_preserves_colimit_mor_iso))); apply pathsinv0; etrans; [apply assoc|]; etrans; [apply cancel_postcomposition; apply (is_inverse_in_precat2 (Ff_right_tensor_preserves_colimit_mor_are_inverses))|]; etrans; [apply id_left|]; apply pathsinv0; etrans; [| use (base_paths _ _ (uniqueness (z_iso_inv (Ff_right_tensor_preserves_colimit_mor_iso) · y,, _))) ]; [reflexivity|]; intro v; etrans; [apply assoc|]; etrans; [|exact (Hy v)]; apply cancel_postcomposition; apply subtypePath; [intro; apply isaprop_section_nat_trans_disp_axioms|]; apply funextsec; intro f; apply subtypePath; [intro; apply isapropdirprod; apply homset_property|]; etrans; [use pr1_transportf_const|]; apply (colimArrowCommutes (CCFf_pt_ob1 CC (mapdiagram (monoidal_right_tensor A) d) f)) ). 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