proposition: Lemma L_map_R_map_elp {C : category} {n : nwfs C} {a b c d : C} {f : a --> b} {g : c --> d} (hf : nwfs_L_maps n f) (hg : nwfs_R_maps n g) : elp f g.
proof: Proof. intros h k H. destruct (R_map_section hf) as [s [Hs0 Hs1]]. destruct (L_map_retraction hg) as [p [Hp0 Hp1]]. set (hk := mors_to_arrow_mor f g h k H). set (Fhk := functor_on_morphisms (fact_functor n) hk). set (Khk := three_mor11 Fhk). set (Hhk := three_mor_comm Fhk). simpl in Hhk. destruct Hhk as [Hhk0 Hhk1]. exists (s · Khk · p). abstract ( split; [ rewrite assoc, assoc; rewrite Hs0; etrans; [apply maponpaths_2; exact Hhk0|]; rewrite <- assoc; etrans; [apply maponpaths; exact Hp1|]; now rewrite id_right | rewrite <- (assoc _ p g); rewrite Hp0; rewrite <- assoc; etrans; [apply maponpaths; exact (pathsinv0 Hhk1)|]; rewrite assoc; etrans; [apply maponpaths_2; exact Hs1|]; now rewrite id_left ] ). Defined.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Monads.Monads UniMath.CategoryTheory.Monads.Comonads UniMath.CategoryTheory.Monads.MonadAlgebras UniMath.CategoryTheory.Monads.ComonadCoalgebras UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.NaturalTransformations UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.DisplayedCats.SIP UniMath.CategoryTheory.DisplayedCats.Examples.Arrow UniMath.CategoryTheory.DisplayedCats.Examples.Three UniMath.CategoryTheory.DisplayedCats.Examples.MonadAlgebras UniMath.ModelCategories.MorphismClass UniMath.ModelCategories.Retract UniMath.ModelCategories.Lifting UniMath.ModelCategories.Helpers