proposition: Lemma K_small_if_J_small : class_presentable J -> preserves_colimits_of_shape K nat_graph.
proof: Proof. intros HJ. intros d cl cc isclCC. set (clCC := make_ColimCocone _ _ _ isclCC). set (Kd00 := project_diagram00 (mapdiagram K d)). set (Kd11 := project_diagram11 (mapdiagram K d)). use (is_z_iso_isColim _ (arrow_colims CC _ (mapdiagram K d))). use tpair. - use mors_to_arrow_mor. * use CoproductArrow. intro S. exact (arrow_mor00 (presentable_lp_colimK_mor isclCC S (HJ _ (pr2 (morcls_lp_map S))))). * use CoproductArrow. intro S. exact (arrow_mor11 (presentable_lp_colimK_mor isclCC S (HJ _ (pr2 (morcls_lp_map S))))). * abstract ( use CoproductArrow_eq; intro S; etrans; [apply assoc|]; etrans; [apply cancel_postcomposition; apply (CoproductInCommutes (morcls_lp_dom_coprod CC J cl))|]; apply pathsinv0; etrans; [apply assoc|]; etrans; [apply cancel_postcomposition; apply (CoproductOfArrows'In _ _ (morcls_lp_dom_coprod CC J cl) _ _ S)|]; etrans; [apply assoc'|]; etrans; [apply cancel_precomposition; apply (CoproductInCommutes (morcls_lp_cod_coprod CC J cl))|]; set (mor := (presentable_lp_colimK_mor isclCC S (HJ _ (pr2 (morcls_lp_map S))))); exact (pathsinv0 (arrow_mor_comm mor)) ). - split. * apply pathsinv0. use (colim_endo_is_identity). intro v. etrans. apply assoc. etrans. apply cancel_postcomposition. apply (colimArrowCommutes). use arrow_mor_eq. + use CoproductArrow_eq. intro S. etrans. apply assoc. etrans. apply cancel_postcomposition. apply (CoproductOfArrowsInclusionIn _ (morcls_lp_dom_coprod CC J (dob d v))). etrans. apply assoc'. etrans. apply id_left. etrans. apply (CoproductInCommutes (morcls_lp_dom_coprod CC J cl) _ (pr1 S,, _)). exact (arrow_mor00_eq (presentable_lp_colimK_mor_coconeInCommutes isclCC S (HJ _ (pr2 (morcls_lp_map S))))). + use CoproductArrow_eq. intro S. etrans. apply assoc. etrans. apply cancel_postcomposition. apply (CoproductOfArrowsInclusionIn _ (morcls_lp_cod_coprod CC J (dob d v))). etrans. apply assoc'. etrans. apply id_left. etrans. apply (CoproductInCommutes (morcls_lp_cod_coprod CC J cl) _ (pr1 S,, _)). exact (arrow_mor11_eq (presentable_lp_colimK_mor_coconeInCommutes isclCC S (HJ _ (pr2 (morcls_lp_map S))))). * use arrow_mor_eq. + use CoproductArrow_eq. intro S. etrans. apply assoc. etrans. apply cancel_postcomposition. apply (CoproductInCommutes (morcls_lp_dom_coprod CC J cl) _ S). apply pathsinv0. etrans. apply id_right. apply pathsinv0. exact (arrow_mor00_eq (presentable_lp_colimK_mor_colimArrowCommutes isclCC S (HJ _ (pr2 (morcls_lp_map S))))). + use CoproductArrow_eq. intro S. etrans. apply assoc. etrans. apply cancel_postcomposition. apply (CoproductInCommutes (morcls_lp_cod_coprod CC J cl) _ S). apply pathsinv0. etrans. apply id_right. apply pathsinv0. exact (arrow_mor11_eq (presentable_lp_colimK_mor_colimArrowCommutes isclCC S (HJ _ (pr2 (morcls_lp_map S))))). Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Isos 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.whiskering UniMath.CategoryTheory.Chains.Chains UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.Colimits UniMath.CategoryTheory.Monads.Monads UniMath.CategoryTheory.Monads.Comonads UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.DisplayedCats.Examples.Arrow UniMath.CategoryTheory.DisplayedCats.Examples.Three UniMath.ModelCategories.MorphismClass UniMath.ModelCategories.NWFS UniMath.ModelCategories.Generated.LiftingWithClass UniMath.ModelCategories.Generated.OneStepMonad UniMath.ModelCategories.Helpers