proposition: Lemma presentable_lp_homSet_colim_colimK_fun_rel_impl (d : chain (arrow C)) {cl : arrow C} (S : morcls_lp J cl) (uS vT : (HSETcobase (pr1 (morcls_lp_map S)) d)) (HuSvT : Colimits.rel _ _ uS vT) : presentable_lp_homSet_colim_colimK_fun_eqrel d S uS vT.
proof: Proof. set (meqrel := @minimal_eqrel_from_hrel _ (Colimits.rel0 _ (homSet_diagram (pr1 (morcls_lp_map S)) d))). set (presfun := presentable_lp_homSet_colim_colimK_fun_eqrel d S). apply (meqrel presfun). - apply (presentable_lp_homSet_colim_colimK_fun_rel0_impl d S). - trivial. 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