proposition: Lemma cop_nwfs_split_epi_is_r_map (g : arrow C) : is_split_epi g -> nwfs_R_maps cop_nwfs g.
proof: Proof. intro Hg. destruct Hg as [g' rel]. use tpair. - use mors_to_arrow_mor. * use BinCoproductArrow. + exact (identity _). + exact g'. * exact (identity _). * abstract ( use BinCoproductArrowsEq; [ etrans; [apply assoc|]; etrans; [apply cancel_postcomposition; apply BinCoproductIn1Commutes|]; etrans; [apply id_left|]; apply pathsinv0; etrans; [apply assoc|]; etrans; [apply cancel_postcomposition; apply BinCoproductIn1Commutes|]; apply id_right | etrans; [apply assoc|]; etrans; [apply cancel_postcomposition; apply BinCoproductIn2Commutes|]; etrans; [exact (rel)|]; apply pathsinv0; etrans; [apply assoc|]; etrans; [apply id_right|]; etrans; [apply BinCoproductIn2Commutes|]; reflexivity ] ). - split; use arrow_mor_eq. * etrans. apply BinCoproductIn1Commutes. reflexivity. * apply id_left. * use BinCoproductArrowsEq. + etrans. apply assoc. etrans. apply cancel_postcomposition. apply BinCoproductIn1Commutes. apply pathsinv0. etrans. apply assoc. etrans. apply cancel_postcomposition. apply BinCoproductIn1Commutes. etrans. apply assoc'. etrans. apply cancel_precomposition. apply BinCoproductIn1Commutes. etrans. apply id_right. use BinCoproductArrowsEq. -- etrans. apply BinCoproductIn1Commutes. apply pathsinv0. etrans. apply assoc. etrans. apply cancel_postcomposition. apply BinCoproductIn1Commutes. etrans. apply BinCoproductIn1Commutes. reflexivity. -- etrans. apply BinCoproductIn2Commutes. apply pathsinv0. etrans. apply assoc. etrans. apply cancel_postcomposition. apply (BinCoproductIn2Commutes _ _ _ (cop_ff_cop g)). etrans. apply BinCoproductIn2Commutes. reflexivity. + etrans. apply assoc. etrans. apply cancel_postcomposition. apply BinCoproductIn2Commutes. etrans. apply BinCoproductIn2Commutes. apply pathsinv0. etrans. apply assoc. etrans. apply cancel_postcomposition. apply BinCoproductIn2Commutes. etrans. apply assoc'. etrans. apply id_left. etrans. apply BinCoproductIn2Commutes. reflexivity. * reflexivity. 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