proposition: Lemma FR_lt_preserves_colim_impl_Ff_lt_preserves_colim_mor_axioms (F : Ff C) (d : chain Ff_mon) (HR : FR_slice_omega_small F) (CL := ChainsFf CC d) (FfCC := ChainsFf CC (mapdiagram (monoidal_left_tensor (F : Ff_mon)) d)) : section_nat_trans_disp_axioms (FR_lt_preserves_colim_impl_Ff_lt_preserves_colim_mor_data F d HR).
proof: Proof. intros f g γ. apply subtypePath; [intro; apply isapropdirprod; apply homset_property|]. etrans. apply pr1_transportf_const. set (HRCC := FR_slice_colimcocone_over_pointwise_tensored F d HR f). use (colimArrowUnique' HRCC). intro v. etrans. apply assoc. etrans. apply cancel_postcomposition. use (pr1_section_disp_on_morphisms_comp F). etrans. apply cancel_postcomposition. set (mor := three_mor_mor12 (section_nat_trans (colimIn CL v) g)). use (section_disp_on_eq_morphisms F (γ' := (#(fact_R (dob d v)) γ · mor))). 1: etrans. apply (colimOfArrowsIn _ _ (CC nat_graph (Ff_diagram_pointwise_ob1 d f))). reflexivity. 1: etrans. apply id_left. apply pathsinv0. apply id_right. etrans. apply cancel_postcomposition. exact (pathsinv0 (pr1_section_disp_on_morphisms_comp F _ _)). etrans. apply assoc'. etrans. apply cancel_precomposition. { etrans. apply cancel_postcomposition. exact (FcolimArrow_coconeInBase_is_colimInHR F d HR g v). set (HRCCg := FR_slice_colimcocone_over_pointwise_tensored F d HR g). apply (colimArrowCommutes HRCCg). } apply pathsinv0. etrans. apply assoc. etrans. apply cancel_postcomposition. apply (colimArrowCommutes HRCC). etrans. apply colimOfArrowsIn. reflexivity. 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