proposition: Lemma nwfs_rlp_L_maps_cl_subs_R_maps_cl {C : category} (n : nwfs C) : rlp ((nwfs_L_maps_class n)^cl) ⊆ ((nwfs_R_maps_class n)^cl).
proof: Proof. intros a b f hf. set (Lf := arrow_mor (fact_L n f)). set (Rf := arrow_mor (fact_R n f)). cbn in Lf, Rf. use (hf _ _ Lf). - apply in_morcls_retc_if_in_morcls. exact (nwfs_Lf_is_L_map n f). - exact (identity _). - exact Rf. - rewrite id_left. apply pathsinv0. exact (LR_compatibility n f). - intro hl. destruct hl as [l [hl0 hl1]]. apply hinhpr. exists _, _, Rf. split. * exact (nwfs_Rf_is_R_map n f). * use make_retract. + exact Lf. + exact l. + exact (identity _). + exact (identity _). + use make_is_retract. -- exact hl0. -- now rewrite id_left. -- rewrite id_right. exact (LR_compatibility n f). -- rewrite id_right. exact hl1. 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