proposition: Lemma nwfs_wfs_closed_transfinite_composition {C : category} {d : chain C} {n : nwfs C} (CC : ColimCocone d) (Hd : chain_L_map d n) : ∑ (f : arrow C), nwfs_L_maps_class n _ _ f × retract f (colimIn CC 0).
proof: Proof. exists (fact_L n (colimIn CC 0)). split; [exact (nwfs_Lf_is_L_map _ _)|]. use make_retract. - exact (identity _). - exact (identity _). - exact (arrow_mor11 (nwfs_tfcomp_alg_map CC Hd)). - exact (fact_R n (colimIn CC 0)). - use make_is_retract. * apply id_left. * apply pathsinv0. use colim_endo_is_identity. intro v. etrans. apply assoc. etrans. apply cancel_postcomposition. apply colimArrowCommutes. exact (nwfs_tfcomp_lp_unit_compat CC Hd v). * etrans. apply id_left. apply pathsinv0. apply colimArrowCommutes. * etrans. apply id_left. apply pathsinv0. exact (three_comp (fact_functor n (colimIn CC 0))). Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Monads.Monads UniMath.CategoryTheory.Monads.MonadAlgebras UniMath.CategoryTheory.Monads.Comonads UniMath.CategoryTheory.Monads.ComonadCoalgebras UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Chains.Chains UniMath.CategoryTheory.DisplayedCats.Examples.Arrow UniMath.CategoryTheory.DisplayedCats.Examples.Three UniMath.ModelCategories.MorphismClass UniMath.ModelCategories.Retract UniMath.ModelCategories.Lifting UniMath.ModelCategories.WFS UniMath.ModelCategories.NWFS UniMath.ModelCategories.Helpers