proposition: Lemma algebraically_free_nwfs_gives_cofibrantly_generated_wfs : algebraically_free -> (nwfs_R_maps_class n)^cl = λ x y f, ∥rlp_morcls_disp J f∥.
proof: Proof. intro H. destruct H as [η cofibη]. apply morcls_eq_impl_morcls_cl_eq. { intros x' y' g' x y g Hg. destruct Hg as [Jg Rgg']. use (hinhuniv _ Jg). clear Jg; intro Jg. apply hinhpr. intros f Jf. apply (@right_lifting_data_retract J g g'). - exact Rgg'. - exact Jg. - exact Jf. } apply morphism_class_subset_antisymm; intros x y f Hf; use (hinhuniv _ Hf); clear Hf; intro Hf; apply hinhpr. - set (θ := R_map_rlp_morcls_structure η). exact (θ f Hf). - set (θinv := right_adjoint_of_is_equiv_over _ cofibη). exact (θinv f Hf). 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.Monads.Monads UniMath.CategoryTheory.Monads.MonadAlgebras UniMath.CategoryTheory.catiso UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Graphs.Coequalizers UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.Limits.Pushouts UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.SIP UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.DisplayedCats.Equivalences UniMath.CategoryTheory.DisplayedCats.Examples.Opposite UniMath.CategoryTheory.DisplayedCats.Examples.Arrow UniMath.CategoryTheory.DisplayedCats.Examples.Three UniMath.ModelCategories.MorphismClass UniMath.ModelCategories.Retract UniMath.ModelCategories.Lifting UniMath.ModelCategories.NWFS UniMath.ModelCategories.NWFSisWFS UniMath.ModelCategories.Helpers