proposition: Lemma osc_preserves_diagram_on (HJ : class_presentable J) : ∏ B, T_preserves_diagram_on LNWFS_tot_monoidal (LNWFS_pointed one_step_comonad_as_LNWFS) (ChainsLNWFS CC) (CoequalizersLNWFS CC) B.
proof: Proof. intro B. intros CC' cl' cc'. set (L1 := LNWFS_pointed one_step_comonad_as_LNWFS). set (d := (free_monoid_coeq_sequence_diagram_on LNWFS_tot_monoidal L1 (CoequalizersLNWFS CC) B )). set (CL := ChainsLNWFS CC d). set (dbase := mapdiagram (pr1_category _) d). use (Ff_lt_preserves_colim_impl_LNWFS_lt_preserves_colim CC L1 d _ cl' cc'). use (FR_lt_preserves_colim_impl_Ff_lt_preserves_colim CC (pr11 L1)). use (FR_slice_omega_small_if_L_omega_small). use (L1_small_if_K_small). apply (K_small_if_J_small). exact HJ. 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.Limits.Coproducts UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Pushouts UniMath.CategoryTheory.Limits.Graphs.Coequalizers UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.whiskering 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.Combinatorics.StandardFiniteSets UniMath.CategoryTheory.Chains.Chains UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.CategoriesOfMonoids UniMath.CategoryTheory.DisplayedCats.Examples.Arrow UniMath.CategoryTheory.DisplayedCats.Examples.Three UniMath.ModelCategories.MorphismClass UniMath.ModelCategories.Generated.LiftingWithClass UniMath.ModelCategories.NWFS UniMath.ModelCategories.Generated.OneStepMonad UniMath.ModelCategories.Generated.GenericFreeMonoid UniMath.ModelCategories.Generated.GenericFreeMonoidSequence UniMath.ModelCategories.Generated.MonoidalHelpers UniMath.ModelCategories.Helpers UniMath.ModelCategories.Generated.MonoidalHelpers UniMath.ModelCategories.Generated.FFMonoidalStructure UniMath.ModelCategories.Generated.LNWFSMonoidalStructure UniMath.ModelCategories.Generated.LNWFSCocomplete UniMath.ModelCategories.Generated.LNWFSClosed UniMath.ModelCategories.Generated.LNWFSSmallnessReduction UniMath.ModelCategories.Generated.OneStepMonadSmall