proposition: Lemma is_model_category_mk' {C : category} {W K AF AK F : morphism_class C} (weq : is_weak_equivalences W) (kaf : is_wfs K AF) (akf : is_wfs AK F) (hAF : AF = F ∩ W) (hAK : AK ⊆ W) : is_model_category W K F.
proof: Proof. use make_is_model_category. - assumption. - rewrite hAF in kaf. assumption. - enough (K ∩ W ⊆ AK) as kw_sak. { assert (K ∩ W = AK) as kw_ak. { apply (morphism_class_subset_antisymm kw_sak). intros a b f hf. split. - rewrite (is_wfs_llp akf) in hf. rewrite (is_wfs_llp kaf). revert a b f hf. apply llp_anti. intros x y g hg. rewrite hAF in hg. destruct hg as [hgf ?]. exact hgf. - exact (hAK _ _ _ hf). } rewrite kw_ak. exact akf. } { intros a b f hf. destruct hf as [f_k f_w]. set (acf_fact := (is_wfs_fact akf) _ _ f). use (hinhuniv _ acf_fact). clear acf_fact; intro acf_fact. destruct acf_fact as [c [g [h [g_ak [h_f gh]]]]]. assert (h_w : (W _ _) h). { specialize (hAK _ _ _ g_ak) as g_w. apply ((is_weq_cancel_left weq) _ _ _ _ _ g_w). rewrite gh. exact f_w. } assert (h_af : (AF _ _) h). { rewrite hAF. split. - exact h_f. - exact h_w. } use (wfs'lp (make_wfs K AF kaf) f_k h_af g (identity b)). { rewrite id_right. exact gh. } intros hl. destruct hl as [l [hl1 hl2]]. assert (r : retract g f). { use (make_retract (identity a) (identity a) l h). use make_is_retract. - now rewrite id_left. - assumption. - rewrite id_left. now symmetry. - rewrite id_left. now symmetry. } exact (wfs_L_retract (make_wfs AK F akf) r g_ak). } Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.ModelCategories.Lifting UniMath.ModelCategories.Retract UniMath.ModelCategories.MorphismClass UniMath.ModelCategories.WFS UniMath.ModelCategories.WeakEquivalences