proposition: Lemma nwfs_Lf_is_L_map {C : category} (n : nwfs C) : ∏ f : arrow C, (nwfs_L_maps_class n) _ _ (arrow_mor (fact_L n f)).
proof: Proof. intro f. apply hinhpr. exists (nwfs_Σ n f). split; use arrow_mor_eq. - etrans. apply cancel_postcomposition. exact (nwfs_Σ_top_map_id n f). apply id_left. - exact (nwfs_Σ_bottom_map_inv n f). - apply cancel_precomposition. apply pathsinv0. etrans. exact (nwfs_Σ_top_map_id n f). apply pathsinv0. exact (nwfs_Σ_top_map_id n (mor_to_arrow_ob _)). - exact (nwfs_Σ_bottom_map_L_is_middle_map_of_Σ _ _). 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