proposition: Lemma FR_lt_preserves_colim_impl_Ff_lt_preserves_colim_mor_pointwise_three_comm (F : Ff C) (d : chain Ff_mon) (HR : FR_slice_omega_small F) (f : arrow C) (CL := ChainsFf CC d) (FfCC := ChainsFf CC (mapdiagram (monoidal_left_tensor (F : Ff_mon)) d)) (base_mor := FR_lt_preserves_colim_impl_Ff_lt_preserves_colim_mor_pointwise F d HR f) : (fact_L (F ⊗_{ Ff_mon} colim CL) f) · z_iso_inv base_mor = (identity _) · (fact_L (colim FfCC) f) × (fact_R (F ⊗_{ Ff_mon} colim CL) f) · (identity _) = z_iso_inv base_mor · (fact_R (colim FfCC) f).
proof: Proof. set (HRCC := FR_slice_colimcocone_over_pointwise_tensored F d HR f). set (baseCC := (CCFf_pt_ob1 CC (mapdiagram (monoidal_left_tensor (F : Ff_mon)) d) f)). split. - apply pathsinv0. etrans. apply id_left. etrans. apply assoc'. apply pathsinv0. etrans. apply assoc'. etrans. apply assoc'. apply cancel_precomposition. etrans. apply assoc. etrans. apply cancel_postcomposition. set (cin0 := colimIn CL 0). set (cin012 := three_mor_mor12 (section_nat_trans cin0 f)). exact (arrow_mor_comm (#(fact_L F) cin012)). etrans. apply assoc'. apply cancel_precomposition. etrans. etrans. apply cancel_postcomposition. exact (FcolimArrow_coconeInBase_is_colimInHR F d HR f 0). apply (colimArrowCommutes HRCC). reflexivity. - etrans. apply id_right. show_id_type. apply (colimArrowUnique' HRCC). intro v. apply pathsinv0. etrans. apply assoc. etrans. apply cancel_postcomposition. apply (colimArrowCommutes HRCC). etrans. apply (colimArrowCommutes baseCC). apply pathsinv0. set (ccpointwise := Ff_cocone_pointwise_R d f). set (RcoconeInBase := #(fact_R F) (coconeIn_colimArrow_mor ccpointwise v)). etrans. exact (arrow_mor_comm RcoconeInBase). apply id_right. Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Pushouts UniMath.CategoryTheory.Limits.Graphs.Coequalizers UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Graphs.EqDiag UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Chains.Chains UniMath.CategoryTheory.slicecat UniMath.CategoryTheory.Monads.Monads UniMath.CategoryTheory.Monads.MonadAlgebras UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.DisplayedCats.Examples.Arrow UniMath.CategoryTheory.DisplayedCats.Examples.Three UniMath.ModelCategories.NWFS UniMath.ModelCategories.Generated.MonoidalHelpers UniMath.ModelCategories.Helpers UniMath.ModelCategories.Generated.LNWFSHelpers UniMath.ModelCategories.Generated.MonoidalHelpers UniMath.ModelCategories.Generated.FFMonoidalStructure UniMath.ModelCategories.Generated.LNWFSMonoidalStructure UniMath.ModelCategories.Generated.LNWFSCocomplete