Library UniMath.CategoryTheory.ModelCategories.WFS

Require Import UniMath.MoreFoundations.All.
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.Opp.

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

Section wfs.

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

Definition lp {M : category} {a x e b : M} (i : a --> x) (p : e --> b) : UU :=
   (g : a --> e) (f : x --> b),
      p g = f i -> l : x --> e, (l i = g) × (p l = f).

Definition isaprop_lp {M : category} {a b x y : M} (f : a --> b) (g : x --> y) : isaprop (lp f g).
Proof.
  do 3 (apply impred_isaprop; intro).
  apply propproperty.
Qed.

Definition lp_hProp {M : category} {a b x y : M} (f : a --> b) (g : x --> y) : hProp :=
    make_hProp (lp f g) (isaprop_lp f g).

Definition llp {M : category} (R : morphism_class M) : (morphism_class M) :=
    λ {a x : M} (i : a --> x), (e b : M) (p : e --> b), ((R _ _) p lp_hProp i p)%logic.

Definition rlp {M : category} (L : morphism_class M) : (morphism_class M) :=
    λ {e b : M} (p : e --> b), (a x : M) (i : a --> x), ((L _ _) i lp_hProp i p)%logic.

Lemma llp_anti {M : category} {R R' : morphism_class M} (h : R R') : llp R' llp R.
Proof.
  unfold "⊆" in *.
  intros a x i H.
  intros e b p K.
  apply (H e b p).
  apply (h e b p).
  exact K.
Defined.

Lemma opp_rlp_is_llp_opp {M : category} (L : morphism_class M) :
    morphism_class_opp (rlp L) = (llp (morphism_class_opp L)).
Proof.
  apply morphism_class_subset_antisymm; intros a b f.
  - intro rlpf.
    intros x y g hg.
    intros top bottom H.
    use (rlpf _ _ (rm_opp_mor g)).
    * exact hg.
    * exact (rm_opp_mor bottom).
    * exact (rm_opp_mor top).
    * symmetry.
      exact H.
    *
      intros hl.
      destruct hl as [l [hlg hlf]].
      apply hinhpr.

      exists (opp_mor l).
      split; assumption.
  - intro rlpf.
    intros x y g hg.
    intros top bottom H.
    use (rlpf _ _ (rm_opp_mor g)).
    * exact hg.
    * exact (rm_opp_mor bottom).
    * exact (rm_opp_mor top).
    * symmetry.
      exact H.
    * intro hl.
      destruct hl as [l [hlg hlf]].
      apply hinhpr.

      exists (opp_mor l).
      split; assumption.
Defined.

Lemma opp_llp_is_rlp_opp {M : category} (L : morphism_class M) :
    morphism_class_opp (llp L) = rlp (morphism_class_opp L).
Proof.
  rewrite <- (morphism_class_opp_opp (rlp _)).
  rewrite (opp_rlp_is_llp_opp _).
  trivial.
Defined.

Definition wfs_fact_ax {M : category} (L R : morphism_class M) :=
    ( x y (f : x --> y), z (g : x --> z) (h : z --> y), (L _ _) g × (R _ _) h × h g = f).

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

Definition make_is_wfs {M : category} {L R : morphism_class M}
    (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 (M : category) :=
   (L R : morphism_class M), is_wfs L R.

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

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

Lemma isaprop_is_wfs {M : category} (L R : morphism_class M) : 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.

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

Lemma wfs_L_retract {M : category} (w : wfs M)
  {a b a' b'} {f : a --> b} {f' : a' --> b'} (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 x y 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.
Defined.

Lemma llp_rlp_self {M : category} (L : morphism_class M) : L llp (rlp L).
Proof.
  intros a b f hf x y g hg.
  apply (hg _ _ _).
  exact hf.
Defined.

Lemma rlp_llp_self {M : category} (L : morphism_class M) : L rlp (llp L).
Proof.
  intros a b f hf x y g hg.
  apply (hg _ _ _).
  exact hf.
Defined.

Lemma wfs_of_factorization {M : category} (I : morphism_class M)
  (h : (x y : M) (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.
Defined.

Lemma retract_argument {M : category} {L' : morphism_class M} (w : wfs M)
  (H : x y (f : x --> y), z (g : x --> z) (h : z --> y), (L' _ _) g × (wfs_R w _ _) h × h g = f) :
   (a b : M) (f : a --> b), (wfs_L w _ _) f -> x' y' (f' : x' --> y') (r : retract f' f), (L' _ _) f'.
Proof.
  intros a b 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 a) (identity a) l h).
    use make_is_retract.
    - now rewrite id_left.
    - assumption.
    - rewrite id_left. now symmetry.
    - rewrite id_left. now symmetry.
  }

  
  apply hinhpr.

  exists a, z, g, r.
  exact hg.
Defined.

Lemma lp_isos_univ {M : category} {a b x y : M} (f : a --> b) (g : x --> y) :
  (morphism_class_isos M _ _ 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.
Defined.

Lemma lp_univ_isos {M : category} {a b x y : M} (f : a --> b) (g : x --> y) :
  (morphism_class_isos M _ _ 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.
Defined.

Lemma llp_univ {M : category} : llp (morphism_class_univ M) = morphism_class_isos M.
Proof.
  apply morphism_class_subset_antisymm; intros a b 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 x y g _.
    exact (lp_isos_univ f g H).
Defined.

Lemma rlp_isos {M : category} : rlp (morphism_class_isos M) = morphism_class_univ M.
Proof.
  apply morphism_class_subset_antisymm.
  -
    intros x y g H.
    unfold morphism_class_univ.
    exact tt.
  -
    rewrite <- llp_univ.
    exact (rlp_llp_self _).
Defined.

Lemma wfs_isos_univ {M : category} : is_wfs (morphism_class_isos M) (morphism_class_univ M).
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 M x).
    * rewrite id_left.
      reflexivity.
Defined.

Definition opp_is_wfs {M : category} {L R : morphism_class M} (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 test.
    simpl in test.
    use (hinhuniv _ test).
    intro H.
    destruct H as [z [g [h [? [? ?]]]]].

    apply hinhpr.
    exists (opp_ob z), (opp_mor h), (opp_mor g).
    repeat split; assumption.
Defined.

Definition opp_wfs {M : category} (w : wfs M) : wfs (op_cat M).
Proof.
  exists (morphism_class_opp (wfs_R w)), (morphism_class_opp (wfs_L w)).
  exact (opp_is_wfs (wfs_is_wfs w)).
Defined.

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

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

Lemma wfs_R_contains_isos {M : category} (w : wfs M) : (morphism_class_isos M) (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)).
Defined.

Lemma wfs_R_retract {M : category} (w : wfs M)
  {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.
Defined.

Lemma wfs_closed_pullbacks {M : category} (w : wfs M)
  {x y z : M} {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.
Defined.

Lemma wfs_closed_pushouts {M : category} (w : wfs M)
    {x y z : M} {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 w)).
Defined.

Lemma wfs_closed_coproducts
    (aoc : AxiomOfChoice)
    {I : hSet} {M : category} (w : wfs M)
    {a b : I -> M} {f : (i : I), a i --> b i} (hf : (i : I), (wfs_L w _ _) (f i))
    (CCa : Coproduct _ _ a) (CCb : Coproduct _ _ b) :
  (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, h (CoproductIn _ _ CCa i)).
  set (ki := λ i, k (CoproductIn _ _ CCb i)).

  assert ( i, li, (li (f i) = hi i) × (g li = 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, (li (f i) = hi i) × (g li = ki i)) as ilift_aoc.
  {
    set (aocI := aoc I).
    simpl in aocI.
    apply (aocI).
    exact ilift.
  }

  
  assert ( (li : ( i, (b i --> x))), ( i, (li i) (f i) = hi i × (g (li i) = 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
    (aoc : AxiomOfChoice)
    {I : hSet} {M : category} (w : wfs M)
    {a b : I -> M} {f : (i : I), b i --> a i} (hf : (i : I), (wfs_R w _ _) (f i))
    (CCa : Product _ _ a) (CCb : Product _ _ b) :
  (wfs_R w _ _) (ProductOfArrows _ _ CCa CCb f).
Proof.
  apply (wfs_closed_coproducts aoc (opp_wfs w)).
  exact hf.
Defined.


Definition wfs_llp' {M : category} (w : wfs M) : (morphism_class M) :=
    λ {x y : M} (f : x --> y), z (g : x --> z) (h : z --> y), (wfs_L w _ _) g × (wfs_R w _ _) h × h g = f × lp_hProp g f.

Definition wfs_rlp' {M : category} (w : wfs M) : (morphism_class M) :=
    λ {x y : M} (f : x --> y), z (g : x --> z) (h : z --> y), (wfs_L w _ _) g × (wfs_R w _ _) h × h g = f × lp_hProp f h.

Lemma llp_iff_lift_with_R {M : category} (w : wfs M) {x y : M} (f : x --> y) : (wfs_llp' w _ _) f <-> (wfs_R w _ _) f.
Proof.
  split.
  - intro hf.
    unfold wfs_R.
    rewrite (wfs_rlp w).

    intros a b g hg.
    intros top bottom comm_total.

    use hf.
    intro h.
    destruct h as [Mf [lf [rf [lf_l [rf_r [fact lp_lff]]]]]].

    use (lp_lff (identity _) rf).
    {
      rewrite id_left.
      now symmetry.
    }
    intro H.
    destruct H as [lift_lff [comm_lff1 comm_lff2]].

    assert (lp_hProp g rf) as lp_grf.
    {
      unfold wfs_R in rf_r.
      rewrite (wfs_rlp) in rf_r.
      exact (rf_r _ _ g hg).
    }

    
    use (lp_grf (lf top) bottom).
    {
      rewrite <- assoc, fact.
      exact comm_total.
    }

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

    apply hinhpr.
    exists (lift_lff lift_grf).

    split.
    * rewrite assoc, comm_grf1, <- assoc, comm_lff1, id_right.
      reflexivity.
    * rewrite <- assoc, comm_lff2.
      exact comm_grf2.
  -
    intro hf.

    use (wfs_fact w _ _ f).
    intro h.
    destruct h as [z [g [h [g_l [h_r comp]]]]].

    apply hinhpr.
    exists z, g, h.
    repeat split; try assumption.

    unfold wfs_R in hf.
    rewrite wfs_rlp in hf.
    exact (hf _ _ _ g_l).
Defined.

Lemma lp_of_retracts {M : category} {a b x y a' b' x' y' : M}
    {f : a --> b} {f' : a' --> b'}
    {g : x --> y} {g' : x' --> y'}
    (rf : retract f' f) (rg : retract g' g) :
  (lp f' g') -> (lp f g).
Proof.
  intros Hlp h k Hcomm.
  destruct rf as [ia [ra [ib [rb [ha [hb [hif hrf]]]]]]].
  destruct rg as [ix [rx [iy [ry [hx [hy [hig hrg]]]]]]].

  use Hlp.
  - exact (ra · h · ix).
  - exact (rb · k · iy).
  - rewrite <- assoc, hig, assoc, <- (assoc _ h g), Hcomm, assoc, hrf, assoc, assoc.
    reflexivity.
  - intro Hl.
    destruct Hl as [l [H1 H2]].

    apply hinhpr.
    exists (ib · l · rx).
    split.
    * rewrite assoc, assoc, <- hif, <- (assoc _ f' l), H1, assoc, assoc.
      now rewrite ha, id_left, <- assoc, hx, id_right.
    * rewrite <- assoc, hrg, assoc, <- (assoc _ l g'), H2, assoc, assoc.
      now rewrite hb, id_left, <- assoc, hy, id_right.
Defined.

End wfs.