proposition: Lemma LNWFS_right_tensor_cocone_isColimCocone : isColimCocone _ _ (monoidal_right_tensor_cocone LNWFS_mon A d (LNWFSCC d)).
proof: Proof. set (colimAL := colim (LNWFSCC (mapdiagram (monoidal_right_tensor A) d))). set (AcolimL := monoidal_right_tensor A (colim (LNWFSCC d))). set (Ffiso := z_iso_inv (Ff_right_tensor_preserves_colimit_mor_iso CC H v0 (pr1 A) dbase)). use (is_z_iso_isColim _ (LNWFSCC (mapdiagram (monoidal_right_tensor A) d))). use tpair. - exists (z_iso_inv Ffiso). exact (LNWFS_right_tensor_preserves_colimit_mor_disp). - abstract ( set (adbase := (mapdiagram (pr1_category (LNWFS C)) (mapdiagram (monoidal_right_tensor A) d))); split; (apply subtypePath; [intro; apply isaprop_lnwfs_mor_axioms|]); [ etrans; [|exact (pr122 Ffiso)]; apply cancel_postcomposition | etrans; [|exact (pr222 Ffiso)]; apply cancel_precomposition ]; (use colimArrowUnique'; intro v; etrans; [apply (colimArrowCommutes (ColimFfCocone CC adbase H v0))|]; apply pathsinv0; etrans; [apply (colimArrowCommutes)|]; 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