proposition: Lemma FR_slice_omega_small_if_L_omega_small (F : Ff C) : preserves_colimits_of_shape (fact_L F) nat_graph -> FR_slice_omega_small F.
proof: Proof. intro HL. intros d y ccy. set (isHLCC := HL _ _ _ (colimArrow_arrow_cocone_isColimCocone ccy)). set (HLCC := make_ColimCocone _ _ _ isHLCC). set (baseCC := arrow_colims CC _ (mapdiagram (fact_L F) (cocone_arrow_chain ccy))). set (base_mor := isColim_is_z_iso _ baseCC _ _ isHLCC). use (is_z_iso_isColim _ (CC _ (fact_cocone_chain F ccy))). exists (arrow_mor11 (pr1 base_mor)). split. - abstract ( apply pathsinv0; use colim_endo_is_identity; intro v; etrans; [apply assoc|]; etrans; [apply cancel_postcomposition; apply colimArrowCommutes|]; exact (arrow_mor11_eq (colimArrowCommutes HLCC _ (colimCocone baseCC) v)) ). - abstract ( etrans; [|exact (arrow_mor11_eq (pr22 base_mor))]; apply cancel_precomposition; use colimArrowUnique; intro v; etrans; [apply colimArrowCommutes|]; 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