proposition: Lemma L1_colim_L1_map_is_inverse_in_precat {g : graph} {d : diagram g (arrow C)} {f : arrow C} {ccf : cocone d f} (HK : preserves_colimit K _ _ ccf) (isclCC : isColimCocone d f ccf) : is_inverse_in_precat (colimArrow (arrow_colims CC _ (mapdiagram (fact_L F1) d)) _ (mapcocone (fact_L F1) d ccf)) (L1_colim_L1_map HK isclCC).
proof: Proof. set (isHKCC := HK isclCC). set (HKCC := make_ColimCocone _ _ _ isHKCC). set (isKfCC := L1_colim_L1_map_dom_Kf_is_colimCocone HK isclCC). set (KfCC := make_ColimCocone _ _ _ isKfCC). set (domfiscc := dom_colim_dom_L1_isColimCocone isclCC). set (domfcc := make_ColimCocone _ _ _ domfiscc). set (iscodKfCC := L1_colim_L1_map_cod_Kf_is_colimCocone HK isclCC). set (codKfCC := make_ColimCocone _ _ _ iscodKfCC). split. - apply pathsinv0. apply colim_endo_is_identity. intro v. etrans. apply assoc. etrans. apply cancel_postcomposition. apply (colimArrowCommutes). use arrow_mor_eq. * exact (colimIn00_L1_colim_L1_commutes HK isclCC v). * use (MorphismsOutofPushoutEqual (isPushout_Pushout (morcls_lp_coprod_diagram_pushout CC J (dob d v)))). + etrans. apply assoc. etrans. apply cancel_postcomposition. apply (PushoutArrow_PushoutIn1). etrans. apply assoc'. etrans. apply cancel_precomposition. apply PushoutArrow_PushoutIn1. exact (colimIn11_Kcolim_colimL1_commutes HK isclCC v). + etrans. apply assoc. etrans. apply cancel_postcomposition. apply (PushoutArrow_PushoutIn2). etrans. apply assoc'. etrans. apply cancel_precomposition. apply PushoutArrow_PushoutIn2. etrans. apply assoc. etrans. apply cancel_postcomposition. exact (colimIn00_L1_colim_L1_commutes HK isclCC v). etrans. apply (colimArrowCommutes (CC _ (project_diagram00 d))). reflexivity. - use arrow_mor_eq. * apply pathsinv0. use (colim_endo_is_identity _ domfcc). intro v. etrans. apply assoc. etrans. apply cancel_postcomposition. exact (colimIn00_L1_colim_L1_commutes HK isclCC v). etrans. apply (colimArrowCommutes (CC _ (project_diagram00 (mapdiagram (fact_L F1) d)))). reflexivity. * use (MorphismsOutofPushoutEqual (isPushout_Pushout (morcls_lp_coprod_diagram_pushout CC J f))). + etrans. apply assoc. etrans. apply cancel_postcomposition. apply PushoutArrow_PushoutIn1. apply pathsinv0. etrans. apply id_right. apply pathsinv0. use (colimArrowUnique' codKfCC). intro v. etrans. apply assoc. etrans. apply cancel_postcomposition. exact (colimIn11_Kcolim_colimL1_commutes HK isclCC v). etrans. apply assoc'. etrans. apply cancel_precomposition. apply (colimArrowCommutes (CC _ (project_diagram11 (mapdiagram (fact_L F1) d)))). etrans. apply PushoutArrow_PushoutIn1. reflexivity. + etrans. apply assoc. etrans. apply cancel_postcomposition. apply PushoutArrow_PushoutIn2. apply pathsinv0. etrans. apply id_right. apply pathsinv0. use (colimArrowUnique' domfcc). intro v. etrans. apply assoc. etrans. apply cancel_postcomposition. etrans. apply assoc. apply cancel_postcomposition. exact (colimIn00_L1_colim_L1_commutes HK isclCC v). etrans. apply cancel_postcomposition. apply (colimArrowCommutes (CC _ (project_diagram00 d))). etrans. apply assoc'. etrans. apply cancel_precomposition. apply (colimArrowCommutes (CC _ (project_diagram11 (mapdiagram (fact_L F1) d)))). etrans. apply PushoutArrow_PushoutIn2. reflexivity. 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