proposition: Lemma wfs_of_factorization (I : morphism_class C) (h : ∏ (x y : C) (f : x --> y), ∃ z (g : x --> z) (h : z --> y), (llp (rlp I) _ _ g) × (rlp I _ _ h) × (h ∘ g = f)) : is_wfs (llp (rlp I)) (rlp I).
proof: Proof. use make_is_wfs. - trivial. - apply morphism_class_subset_antisymm; intros x y g hg. * exact (rlp_llp_self _ _ _ _ hg). * intros a b f hf. apply (hg _ _ _). exact (llp_rlp_self _ _ _ _ hf). - exact h. Qed.
imports: UniMath.MoreFoundations.All UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Limits.Pushouts UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.Limits.Products UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Opp UniMath.CategoryTheory.Chains.Chains UniMath.CategoryTheory.DisplayedCats.Examples.Arrow UniMath.ModelCategories.Retract UniMath.ModelCategories.MorphismClass UniMath.ModelCategories.Lifting