Library UniMath.CategoryTheory.ModelCategories.ModelCategories

Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Prelude.

Require Import UniMath.CategoryTheory.ModelCategories.Retract.
Require Import UniMath.CategoryTheory.ModelCategories.MorphismClass.
Require Import UniMath.CategoryTheory.ModelCategories.WFS.
Require Import UniMath.CategoryTheory.ModelCategories.WeakEquivalences.

Section modelcat.

Local Open Scope cat.
Local Open Scope morcls.
Local Open Scope retract.

Definition is_model_category {M : category} (W C F : morphism_class M) :=
    is_weak_equivalences W × is_wfs C (F ∩ W) × is_wfs (C ∩ W) F.

Definition make_is_model_category {M : category} (W C F : morphism_class M)
    (weq : is_weak_equivalences W) (cfw_wfs : is_wfs C (F ∩ W)) (cwf_wfs : is_wfs (C ∩ W) F) : is_model_category W C F :=
  make_dirprod weq (make_dirprod cfw_wfs cwf_wfs).

Definition model_category (M : category) :=
  ∑ (W C F : morphism_class M), is_model_category W C F.

Lemma isprop_is_model_category {M : category} (W C F : morphism_class M) : isaprop (is_model_category W C F).
Proof.
  apply isapropdirprod.
  apply isaprop_is_weak_equivalences.
  apply isapropdirprod; apply isaprop_is_wfs.
Defined.

Lemma is_model_category_mk' {M : category} {W C AF AC F : morphism_class M}
    (weq : is_weak_equivalences W)
    (caf : is_wfs C AF) (acf : is_wfs AC F)
    (hAF : AF = F ∩ W) (hAC : AC ⊆ W) :
    is_model_category W C F.
Proof.
  use make_is_model_category.
  - assumption.   - rewrite hAF in caf.     assumption.
  -
    enough (C ∩ W ⊆ AC) as cw_sac.
    {
      
      assert (C ∩ W = AC) as cw_ac.
      {
        
        apply (morphism_class_subset_antisymm cw_sac).
        intros a b f hf.
        split.
        -
          rewrite (is_wfs_llp acf) in hf.
          rewrite (is_wfs_llp caf).
          revert a b f hf.
          apply llp_anti.
          intros x y g hg.
          rewrite hAF in hg.
          destruct hg as [hgf ?].
          exact hgf.
        -
          exact (hAC _ _ _ hf).
      }
      
      rewrite cw_ac.
      exact acf.
    }
    {
      
      intros a b f hf.
      destruct hf as [f_c f_w].

      use ((is_wfs_fact acf) _ _ f).
      intro H.
      destruct H as [c [g [h [g_ac [h_f gh]]]]].

      assert (h_w : (W _ _) h).
      {
        
        specialize (hAC _ _ _ g_ac) 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 C AF caf) f_c 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 AC F acf) r g_ac).
    }
Defined.

End modelcat.