proposition: Lemma L_map_retraction_comm {C : category} {n : nwfs C} {c d : C} {g : c --> d} (hg : nwfs_R_maps n g) (p := pr111 hg) : p · g = arrow_mor (fact_R n g) × arrow_mor (fact_L n g) · p = identity _.
proof: Proof. set (idd := pr211 hg). set (αgcomm := pr21 hg). set (hαgη := pr12 hg). cbn in p, idd, αgcomm. simpl in hαgη. assert (idd = identity d) as Hidd. { set (bottom_line := dirprod_pr2 (pathsdirprodweq (base_paths _ _ hαgη))). rewrite id_left in bottom_line. exact bottom_line. } split. - specialize (αgcomm) as αgcomm'. unfold idd in Hidd. rewrite Hidd, id_right in αgcomm'. exact αgcomm'. - set (top_line := dirprod_pr1 (pathsdirprodweq (base_paths _ _ hαgη))). exact top_line. Qed.
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