proposition: Lemma presentable_lp_homSet_colim_colimK_fun_rel0_impl (d : chain (arrow C)) {cl : arrow C} (S' : morcls_lp J cl) (uS vT : (HSETcobase (pr1 (morcls_lp_map S')) d)) (HuSvT : Colimits.rel0 _ _ uS vT) : presentable_lp_homSet_colim_colimK_fun_eqrel d S' uS vT.
proof: Proof. use HuSvT. clear HuSvT. intro H; simpl. destruct H as [f Hf]. destruct uS as [u Su]. destruct vT as [v Tv]. unfold presentable_lp_homSet_colim_colimK_fun. cbn in f. induction f. etrans. apply maponpaths. set (ccincomm := colimInCommutes (arrow_colims CC nat_graph (mapdiagram K d)) _ _ (idpath (S u))). exact (pathsinv0 ccincomm). rewrite assoc. apply (cancel_postcomposition _ _ (colimIn (arrow_colims CC nat_graph (mapdiagram K d)) (S u))). use arrow_mor_eq. - etrans. apply (CoproductOfArrowsInclusionIn _ (morcls_lp_dom_coprod CC J (dob d u)) _ _ (morcls_lp_map S',, Su)). etrans. apply id_left. cbn. morcls_lp_coproduct_in_eq. use arrow_mor_eq. * use (pathscomp1 (arrow_mor00_eq Hf)); [|reflexivity]. etrans. apply assoc'. apply id_left. * use (pathscomp1 (arrow_mor11_eq Hf)); [|reflexivity]. etrans. apply assoc'. apply id_left. - etrans. apply (CoproductOfArrowsInclusionIn _ (morcls_lp_cod_coprod CC J (dob d u)) _ _ (morcls_lp_map S',, Su)). etrans. apply id_left. cbn. morcls_lp_coproduct_in_eq. use arrow_mor_eq. * use (pathscomp1 (arrow_mor00_eq Hf)); [|reflexivity]. etrans. apply assoc'. apply id_left. * use (pathscomp1 (arrow_mor11_eq Hf)); [|reflexivity]. etrans. apply assoc'. apply id_left. 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