Library UniMath.ModelCategories.WFS

Require Import UniMath.MoreFoundations.All.
Require Import UniMath.MoreFoundations.Tactics.
Require Import UniMath.CategoryTheory.Core.Prelude.
Require Import UniMath.CategoryTheory.opp_precat.
Require Import UniMath.CategoryTheory.Limits.Pullbacks.
Require Import UniMath.CategoryTheory.Limits.Pushouts.
Require Import UniMath.CategoryTheory.Limits.Coproducts.
Require Import UniMath.CategoryTheory.Limits.Products.
Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits.
Require Import UniMath.CategoryTheory.Limits.Opp.

Require Import UniMath.CategoryTheory.Chains.Chains.

Require Import UniMath.CategoryTheory.DisplayedCats.Examples.Arrow.
Require Import UniMath.ModelCategories.Retract.
Require Import UniMath.ModelCategories.MorphismClass.
Require Import UniMath.ModelCategories.Lifting.

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

Section wfs.

Definition wfs_fact_ax {C : category} (L R : morphism_class C) :=
  ∏ x y (f : x --> y),
    ∃ ef (l : x --> ef) (r : ef --> y),
      (L _ _) l × (R _ _) r × l · r = f.

Definition is_wfs {C : category} (L R : morphism_class C) :=
  (L = llp R) × (R = rlp L) × (wfs_fact_ax L R).

Definition make_is_wfs {C : category} {L R : morphism_class C}
    (llp : L = llp R) (rlp : R = rlp L) (fact : wfs_fact_ax L R) : is_wfs L R :=
  make_dirprod llp (make_dirprod rlp fact).

Definition wfs (C : category) :=
  ∑ (L R : morphism_class C), is_wfs L R.

Definition make_wfs {C : category} (L R : morphism_class C) (w : is_wfs L R) : wfs C :=
  tpair _ L (tpair _ R w).

Definition wfs_L {C : category} (w : wfs C) := (pr1 w).
Definition wfs_R {C : category} (w : wfs C) := pr1 (pr2 w).
Definition is_wfs_llp {C : category} {L R : morphism_class C} (w : is_wfs L R) := pr1 w.
Definition is_wfs_rlp {C : category} {L R : morphism_class C} (w : is_wfs L R) := pr1 (pr2 w).
Definition is_wfs_fact {C : category} {L R : morphism_class C} (w : is_wfs L R) := pr2 (pr2 w).
Definition wfs_is_wfs {C : category} (w : wfs C) := pr2 (pr2 w).
Definition wfs_llp {C : category} (w : wfs C) := is_wfs_llp (wfs_is_wfs w).
Definition wfs_rlp {C : category} (w : wfs C) := is_wfs_rlp (wfs_is_wfs w).
Definition wfs_fact {C : category} (w : wfs C) := is_wfs_fact (wfs_is_wfs w).

Lemma isaprop_is_wfs {C : category} (L R : morphism_class C) :
    isaprop (is_wfs L R).
Proof.
  apply isapropdirprod.
  - unfold isaprop.
    exact (isasetmorphism_class _ _).
  - apply isapropdirprod.
    * exact (isasetmorphism_class _ _).
    * do 3 (apply impred_isaprop; intro).
      apply propproperty.
Qed.

Context {C : category}.

Lemma wfs'lp (w : wfs C)
    {x y a b} {f : x --> y} {g : a --> b}
    (hf : (wfs_L w _ _) f) (hg : (wfs_R w _ _) g) :
  lp f g.
Proof.
  unfold wfs_L in hf.
  rewrite (wfs_llp w) in hf.
  exact (hf _ _ _ hg).
Qed.

Lemma wfs_L_retract (w : wfs C)
    {x y x' y' : C} {f : x --> y} {f' : x' --> y'}
    (r : retract f f') (hf : (wfs_L w _ _) f) :
  (wfs_L w _ _) f'.
Proof.
  destruct r as [ia [ra [ib [rb [ha [hb [hi hr]]]]]]].

  unfold wfs_L.
  rewrite (wfs_llp w).
  intros a b g hg h k s.
  use (wfs'lp w hf hg (h ∘ ra) (k ∘ rb) _).
  {
    rewrite <- assoc, s, assoc, assoc, hr.
    reflexivity.
  }
  
  intro hl.
  destruct hl as [l [hlh hlk]].

  apply hinhpr.
  exists (l ∘ ib).
  split.
  * rewrite assoc, <- hi, <- assoc, hlh, assoc, ha, id_left.
    reflexivity.
  * rewrite <- assoc, hlk, assoc, hb, id_left.
    reflexivity.
Qed.

Lemma llp_rlp_self (L : morphism_class C) : L ⊆ llp (rlp L).
Proof.
  intros a b f hf x y g hg.
  apply (hg _ _ _).
  exact hf.
Qed.

Lemma rlp_llp_self (L : morphism_class C) : L ⊆ rlp (llp L).
Proof.
  intros a b f hf x y g hg.
  apply (hg _ _ _).
  exact hf.
Qed.

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.
  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.

Lemma retract_argument {L' : morphism_class C} (w : wfs C)
    (H : wfs_fact_ax L' (wfs_R w)) :
  ∏ {x y} (f : x --> y),
    (wfs_L w _ _) f
    -> ∃ {x' y'} (f' : x' --> y') (r : retract f' f), (L' _ _) f'.
Proof.
  intros x y f hf.

  specialize (H _ _ f) as eHf.
  simpl in eHf.
  use (hinhuniv _ eHf).
  intro Hf.
  destruct Hf as [z [g [h [hg [hh hgh]]]]].

  use (wfs'lp w hf hh g (identity _)).
  {
    rewrite hgh, id_right.
    reflexivity.
  }
  intro hl.
  destruct hl as [l [hl1 hl2]].

  assert (r : retract g f).
  {
    use (make_retract (identity _) (identity _) l h).
    use make_is_retract.
    - now rewrite id_left.
    - assumption.
    - rewrite id_left. now symmetry.
    - rewrite id_left. now symmetry.
  }

  
  apply hinhpr.

  exists x, z, g, r.
  exact hg.
Qed.

Lemma lp_isos_univ {x y a b : C} (f : x --> y) (g : a --> b) :
  (morphism_class_isos C _ _ f) -> lp f g.
Proof.
  intro H.
  set (fiso := make_iso _ H).
  change (lp fiso g).

  intros h k s.
  apply hinhpr.
  exists (h ∘ (inv_from_iso fiso)).
  split.
  * rewrite assoc, iso_inv_after_iso, id_left.
    reflexivity.
  * rewrite <- assoc, s, assoc.
    rewrite iso_after_iso_inv, id_left.
    reflexivity.
Qed.

Lemma lp_univ_isos {x y a b : C} (f : x --> y) (g : a --> b) :
  (morphism_class_isos C _ _ f) -> lp g f.
Proof.
  intro H.
  set (fiso := make_iso _ H).
  change (lp g fiso).

  intros h k s.
  apply hinhpr.
  exists ((inv_from_iso fiso) ∘ k).
  split.
  * rewrite assoc, <- s, <- assoc, iso_inv_after_iso, id_right.
    reflexivity.
  * rewrite <- assoc, iso_after_iso_inv, id_right.
    reflexivity.
Qed.

Lemma llp_univ : llp (morphism_class_univ C) = morphism_class_isos C.
Proof.
  apply morphism_class_subset_antisymm; intros x y f H.
  -
    specialize ((H _ _ f) tt).
    use (H (identity _) (identity _)).
    {
      
      rewrite id_left, id_right.
      reflexivity.
    }
    
    intro hl.
    destruct hl as [l [hfl hlf]].
    unfold morphism_class_isos.

    assert (is_z_isomorphism f) as f_z_iso.
    {
      exists l.
      split; assumption.
    }
    
    apply is_iso_from_is_z_iso.
    exact f_z_iso.
  - intros a b g _.
    exact (lp_isos_univ f g H).
Qed.

Lemma rlp_isos : rlp (morphism_class_isos C) = morphism_class_univ C.
Proof.
  apply morphism_class_subset_antisymm.
  -
    intros x y g H.
    unfold morphism_class_univ.
    exact tt.
  -
    rewrite <- llp_univ.
    exact (rlp_llp_self _).
Qed.

Lemma wfs_isos_univ : is_wfs (morphism_class_isos C) (morphism_class_univ C).
Proof.
  use make_is_wfs; try symmetry.
  - exact llp_univ.
  - exact rlp_isos.
  -
    intros x y f.
    apply hinhpr.
    exists x, (identity x), f.

    repeat split.
    * exact (identity_is_iso C x).
    * rewrite id_left.
      reflexivity.
Qed.

Definition opp_is_wfs {L R : morphism_class C} (w : is_wfs L R) :
    is_wfs (morphism_class_opp R) (morphism_class_opp L).
Proof.
  use make_is_wfs.
  - rewrite (is_wfs_rlp w).
    exact (opp_rlp_is_llp_opp _).
  - rewrite (is_wfs_llp w).
    exact (opp_llp_is_rlp_opp _).
  - intros x y f.
    specialize ((is_wfs_fact w) _ _ (rm_opp_mor f)) as H.
    use (hinhuniv _ H).
    clear H; intro H.
    destruct H as [z [g [h [? [? ?]]]]].
    apply hinhpr.
    exists (opp_ob z), (opp_mor h), (opp_mor g).
    repeat split; assumption.
Qed.

Definition opp_wfs (w : wfs C) : wfs (op_cat C).
Proof.
  exists (morphism_class_opp (wfs_R w)), (morphism_class_opp (wfs_L w)).
  exact (opp_is_wfs (wfs_is_wfs w)).
Defined.

End wfs.

Section properties.

Lemma wfs_L_contains_isos {C : category} (w : wfs C) :
    (morphism_class_isos C) ⊆ (wfs_L w).
Proof.
  rewrite <- llp_univ.
  unfold wfs_L.
  rewrite (wfs_llp w).

  apply llp_anti.
  intros x y f hf.
  exact tt.
Qed.

Lemma wfs_R_contains_isos {C : category} (w : wfs C) :
    (morphism_class_isos C) ⊆ (wfs_R w).
Proof.
  intros x y f hf.
  set (opp_containment := wfs_L_contains_isos (opp_wfs w)).
  exact (opp_containment _ _ (opp_mor f) (opp_is_iso _ hf)).
Qed.

Lemma wfs_R_retract {C : category} (w : wfs C)
    {a b a' b'} {f : a --> b} {f' : a' --> b'}
    (r : retract f f') (hf : (wfs_R w _ _) f) :
  (wfs_R w _ _) f'.
Proof.
  use (wfs_L_retract (opp_wfs w) (opp_retract r)).
  exact hf.
Qed.

Lemma wfs_closed_pullbacks {C : category} (w : wfs C)
    {x y z : C} {p : x --> y} {f : z --> y}
    (Pb : Pullback f p) :
  ((wfs_R w _ _) p) -> ((wfs_R w _ _) (PullbackPr1 Pb)).
Proof.
  intro p_r.

  destruct Pb as [[zfx [f'p p2]] [H isPb]].
  simpl in *.
  cbn.

  unfold wfs_R.
  rewrite (wfs_rlp w).
  intros a b i i_l.

  intros p1 g Hp1g.


  unfold wfs_R in p_r.
  rewrite (wfs_rlp w) in p_r.

  use (p_r _ _ i i_l (p2 ∘ p1) (f ∘ g) _).
  {
    rewrite <- assoc, <- H, assoc, Hp1g, assoc.
    reflexivity.
  }

  
  intro hl.
  destruct hl as [l [hl1 hl2]].
  symmetry in hl2.

  destruct (isPb _ g l hl2) as [[gh [hgh1 hgh2]] _].

  apply hinhpr.
  exists gh.
  split.
  -
    apply (MorphismsIntoPullbackEqual isPb).
    * rewrite <-assoc, hgh1, Hp1g.
      reflexivity.
    * rewrite <- assoc, hgh2, hl1.
      reflexivity.
  -
    exact hgh1.
Qed.

Lemma wfs_closed_pushouts {C : category} (w : wfs C)
    {x y z : C} {p : x --> y} {f : x --> z}
    (Po : Pushout f p) :
  ((wfs_L w _ _) p) -> ((wfs_L w _ _) (PushoutIn1 Po)).
Proof.
  apply (wfs_closed_pullbacks (opp_wfs _)).
Qed.

Lemma wfs_closed_coproducts {C : category} {I : hSet} (w : wfs C)
    {a b : I -> C}
    {f : ∏ (i : I), a i --> b i} (hf : ∀ (i : I), (wfs_L w _ _) (f i))
    (CCa : Coproduct _ _ a) (CCb : Coproduct _ _ b)
    (aoc : AxiomOfChoice) :
  (wfs_L w _ _) (CoproductOfArrows _ _ CCa CCb f).
Proof.
  unfold wfs_L in *.
  rewrite (wfs_llp w) in *.
  intros x y g hg.
  intros h k s.

  set (hi := λ i, (CoproductIn _ _ CCa i) · h).
  set (ki := λ i, (CoproductIn _ _ CCb i) · k).

  assert (∏ i, ∃ li, ((f i) · li = hi i) × (li · g = ki i)) as ilift.
  {
    intro i.
    specialize (hf i _ _ g hg) as H.
    specialize (H (hi i) (ki i)).

    use H.

    unfold hi, ki.
    rewrite <- assoc, s, assoc, assoc.
    now rewrite (CoproductOfArrowsIn _ _).
  }

  
  assert (∥∏ i, ∑ li, ((f i) · li = hi i) × (li · g = ki i)∥) as ilift_aoc.
  {
    set (aocI := aoc I).
    simpl in aocI.
    apply (aocI).
    exact ilift.
  }

  
  assert (∃ (li : (∏ i, (b i --> x))), (∏ i, (f i) · (li i) = hi i × ((li i) · g = ki i))) as ilifts.
  {
    use (hinhuniv _ ilift_aoc).
    intro ilift_aoc_sig.
    apply hinhpr.

    use tpair.
    - intro i.
      set (li := ilift_aoc_sig i).
      destruct li as [l hl].
      exact l.
    - intro i.
      set (li := ilift_aoc_sig i).
      simpl.
      destruct li as [l hl].
      exact hl.
  }

  use (hinhuniv _ ilifts).
  intro ilift_sig.
  destruct ilift_sig as [li hli].

  set (hl := isCoproduct_Coproduct _ _ CCb x li).
  destruct hl as [[l hl] uniqueness].

  apply hinhpr.
  exists l.
  split; rewrite CoproductArrowEta, (CoproductArrowEta _ _ _ _ _ l).
  -
    rewrite (precompWithCoproductArrow).

    apply CoproductArrowUnique.

    intro i.
    rewrite CoproductInCommutes.

    destruct (hli i) as [hlicomm _].

    change (CoproductIn _ _ _ _ · h) with (hi i).
    rewrite (hl i).
    exact hlicomm.
  -
    apply CoproductArrowUnique.

    intro i.
    rewrite assoc.
    rewrite CoproductInCommutes.

    destruct (hli i) as [_ klicomm].

    change (CoproductIn _ _ _ _ · k) with (ki i).
    rewrite (hl i).
    exact klicomm.
Qed.

Lemma wfs_closed_products {C : category} {I : hSet} (w : wfs C)
    {a b : I -> C} {f : ∏ (i : I), b i --> a i}
    (hf : ∀ (i : I), (wfs_R w _ _) (f i))
    (CCa : Product _ _ a) (CCb : Product _ _ b)
    (aoc : AxiomOfChoice) :
  (wfs_R w _ _) (ProductOfArrows _ _ CCa CCb f).
Proof.
  apply (wfs_closed_coproducts (opp_wfs w)).
  - exact hf.
  - exact aoc.
Qed.



Lemma llp_iff_lift_with_R {C : category} (w : wfs C) {x y : C} (f : x --> y)
  (H : ∑ z (g : x --> z) (h : z --> y), (wfs_L w _ _) g × (wfs_R w _ _) h × h ∘ g = f) :
    lp (pr12 H) f <-> (wfs_R w _ _) f.
Proof.
  destruct H as [z [g [h [Lg [Rh Hgh]]]]].

  split.
  - intro hf.
    unfold wfs_R.
    rewrite (wfs_rlp w).

    intros a b g' hg'.
    intros top bottom comm_total.

    use (hf (identity _) h).
    {
      rewrite id_left.
      apply pathsinv0.

      exact (Hgh).
    }
    intro h'.
    destruct h' as [lift_lff [comm_lff1 comm_lff2]].

    assert (lp g' h) as lp_grf.
    {
      set (rf_r := Rh).
      unfold wfs_R in rf_r.
      rewrite (wfs_rlp w) in rf_r.
      exact (rf_r _ _ g' hg').
    }

    
    use (lp_grf (g ∘ top) bottom).
    {
      rewrite <- assoc.
      rewrite (Hgh).
      exact comm_total.
    }

    intro H.
    destruct H as [lift_grf [comm_grf1 comm_grf2]].

    apply hinhpr.
    exists (lift_lff ∘ lift_grf).

    split.
    * etrans. apply assoc.
      etrans. apply cancel_postcomposition.
              exact comm_grf1.
      etrans. apply assoc'.
      etrans. apply cancel_precomposition.
              exact comm_lff1.
      apply id_right.
    * etrans. apply assoc'.
      etrans. apply cancel_precomposition.
              exact comm_lff2.
      exact comm_grf2.
  -
    intro hf.
    intros h' k Hk.

    unfold wfs_R in hf.
    rewrite wfs_rlp in hf.
    use hf.
    exact (Lg).
Qed.

End properties.