proposition: Lemma cop_nwfs_r_map_is_split_epi (g : arrow C) : nwfs_R_maps cop_nwfs g -> is_split_epi g.
proof: Proof. intro Rg. destruct Rg as [αg αgax]. use tpair. - exact (BinCoproductIn2 _ · (arrow_mor00 αg)). - etrans. apply assoc'. etrans. apply cancel_precomposition. exact (arrow_mor_comm αg). etrans. apply assoc. etrans. apply cancel_postcomposition. apply (BinCoproductIn2Commutes). exact (arrow_mor11_eq (pr1 αgax)). Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Categories.HSET.All UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Epis UniMath.CategoryTheory.SplitMonicsAndEpis UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.Monads.Monads UniMath.CategoryTheory.Monads.Comonads UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.ModelCategories.MorphismClass UniMath.ModelCategories.NWFS UniMath.ModelCategories.Helpers UniMath.ModelCategories.Generated.LiftingWithClass UniMath.CategoryTheory.DisplayedCats.Examples.Arrow UniMath.CategoryTheory.DisplayedCats.Examples.Three