Library UniMath.CategoryTheory.ModelCategories.NWFS

Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Prelude.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.opp_precat.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.PrecategoryBinProduct.
Require Import UniMath.CategoryTheory.whiskering.
Require Import UniMath.CategoryTheory.Monads.Monads.
Require Import UniMath.CategoryTheory.Monads.MonadAlgebras.

Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Total.
Require Import UniMath.CategoryTheory.DisplayedCats.Functors.
Require Import UniMath.CategoryTheory.DisplayedCats.NaturalTransformations.
Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.

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

Local Open Scope cat.
Local Open Scope mor_disp.

Section Face_maps.

Context (C : category).

Definition face_map_1 : three C arrow C := pr1_category _.

Definition face_map_0_data : functor_data (three C) (arrow C).
Proof.
  use make_functor_data.
  - intro xxx.
    use tpair.
    * exact (make_dirprod (three_ob1 xxx) (three_ob2 xxx)).
    * simpl.
      exact (three_mor12 xxx).
  - intros xxx yyy fff.
    simpl.
    use tpair.
    * split; simpl.
      + exact (three_mor11 fff).
      + exact (three_mor22 fff).
    * simpl.
      symmetry.
      exact (pr2 (three_mor_comm fff)).
Defined.

Definition face_map_0 : three C arrow C.
Proof.
  use make_functor.
  - exact face_map_0_data.
  - split.
    *
      intro.
      apply subtypePath.
      + intro; apply homset_property.
      + trivial.
    *
      intros a b c f g.
      apply subtypePath.
      + intro; apply homset_property.
      + trivial.
Defined.

Definition face_map_2_data : functor_data (three C) (arrow C).
Proof.
  use make_functor_data.
  - intro xxx.
    use tpair.
    * exact (make_dirprod (three_ob0 xxx) (three_ob1 xxx)).
    * simpl.
      exact (three_mor01 xxx).
  - intros xxx yyy fff.
    simpl.
    use tpair.
    * split; simpl.
      + exact (three_mor00 fff).
      + exact (three_mor11 fff).
    * simpl.
      symmetry.
      exact (pr1 (three_mor_comm fff)).
Defined.

Definition face_map_2 : three C arrow C.
Proof.
  use make_functor.
  - exact face_map_2_data.
  - split.
    *
      intro.
      apply subtypePath.
      + intro; apply homset_property.
      + trivial.
    *
      intros a b c f g.
      apply subtypePath.
      + intro; apply homset_property.
      + trivial.
Defined.

Lemma face_compatibility (fg : three C) : arrow_mor (face_map_0 fg) arrow_mor (face_map_2 fg) = arrow_mor (face_map_1 fg).
Proof.
  exact (three_comp fg).
Defined.

Definition c_21_data : nat_trans_data face_map_2 face_map_1.
Proof.
  intro xxx.
  simpl.
  exists (make_dirprod (identity _) (three_mor12 xxx)).
  simpl.
  rewrite id_left.
  symmetry.
  exact (three_comp xxx).
Defined.

Definition c_21 : face_map_2 face_map_1.
Proof.
  use make_nat_trans.
  - exact c_21_data.
  -
    intros xxx yyy ff.

    apply subtypePath.
    *
      intro f.
      simpl.
      apply homset_property.
    *
      cbn.
      rewrite id_left, id_right.
      apply pathsdirprod; trivial.
      symmetry.
      exact (pr2 (three_mor_comm ff)).
Defined.

Definition c_10_data : nat_trans_data face_map_1 face_map_0.
Proof.
  intro xxx.
  simpl.
  exists (make_dirprod (three_mor01 xxx) (identity _)).
  simpl.
  rewrite id_right.
  exact (three_comp xxx).
Defined.

Definition c_10 : face_map_1 face_map_0.
Proof.
  use make_nat_trans.
  - exact c_10_data.
  - intros xxx yyy ff.
    apply subtypePath.
    * intro x.
      apply homset_property.
    * cbn.
      rewrite id_left, id_right.
      apply pathsdirprod; trivial.
      symmetry.
      exact (pr1 (three_mor_comm ff)).
Defined.

End Face_maps.

Arguments face_map_0 {_}.
Arguments face_map_1 {_}.
Arguments face_map_2 {_}.



Definition functorial_factorization (C : category) := section_disp (three_disp C).
Definition fact_section {C : category} (F : functorial_factorization C)
    := section_disp_data_from_section_disp F.
Definition fact_functor {C : category} (F : functorial_factorization C) : arrow C three C :=
    section_functor F.
Coercion fact_functor : functorial_factorization >-> functor.

Lemma functorial_factorization_splits_face_map_1 {C : category} (F : functorial_factorization C) :
    F face_map_1 = functor_identity (arrow C).
Proof.
  apply functor_eq; trivial.
  apply homset_property.
Defined.

Definition fact_L {C : category} (F : functorial_factorization C) : arrow C arrow C :=
    F face_map_2.
Definition fact_R {C : category} (F : functorial_factorization C) : arrow C arrow C :=
    F face_map_0.

Lemma LR_compatibility {C : category} (F : functorial_factorization C) :
     (f : arrow C), arrow_mor (fact_L F f) · arrow_mor (fact_R F f) = arrow_mor f.
Proof.
  intro.
  exact (three_comp _).
Defined.

Definition Φ {C : category} (F : functorial_factorization C) :
    (fact_L F) (functor_identity (arrow C)) :=
  pre_whisker F (c_21 C).

Definition Λ {C : category} (F : functorial_factorization C) :
    (functor_identity (arrow C)) (fact_R F) :=
  pre_whisker F (c_10 C).

Definition R_monad_data {C : category} (F : functorial_factorization C)
  (Π : (fact_R F) (fact_R F) (fact_R F))
  : disp_Monad_data (fact_R F)
  := Π ,, Λ F.

Definition R_monad {C : category} (F : functorial_factorization C)
    (Π : (fact_R F) (fact_R F) (fact_R F))
    (R : disp_Monad_laws (R_monad_data F Π)) : Monad (arrow C) :=
  (fact_R F ,, R_monad_data F Π,, R).

Definition L_monad_data {C : category} (F : functorial_factorization C)
  (Σ : (fact_L F) (fact_L F) (fact_L F))
  : @disp_Monad_data (op_cat (arrow C)) (functor_opp (fact_L F))
  := op_nt Σ ,, op_nt (Φ F).

Definition L_monad {C : category} (F : functorial_factorization C)
    (Σ : (fact_L F) (fact_L F) (fact_L F))
    (L : disp_Monad_laws (L_monad_data F Σ)) : Monad (op_cat (arrow C)) :=
  (functor_opp (fact_L F) ,, L_monad_data F Σ,, L).

Definition nwfs (C : category) :=
     (F : functorial_factorization C) (Σ : (fact_L F) (fact_L F) (fact_L F)) (Π : (fact_R F) (fact_R F) (fact_R F)) ,
    (disp_Monad_laws (L_monad_data F Σ)) × (disp_Monad_laws (R_monad_data F Π)).

Definition make_nwfs {C : category} (F : functorial_factorization C)
    (Σ : (fact_L F) (fact_L F) (fact_L F)) (L : disp_Monad_laws (L_monad_data F Σ))
    (Π : (fact_R F) (fact_R F) (fact_R F)) (R : disp_Monad_laws (R_monad_data F Π))
        : nwfs C.
Proof.
  exists F, Σ, Π.
  exact (make_dirprod L R).
Defined.

Definition nwfs_fact {C : category} (n : nwfs C) := pr1 n.
Coercion nwfs_fact : nwfs >-> functorial_factorization.
Definition nwfs_Σ {C : category} (n : nwfs C) := pr12 n.
Definition nwfs_Π {C : category} (n : nwfs C) := pr122 n.
Definition nwfs_Σ_laws {C : category} (n : nwfs C) := pr1 (pr222 n).
Definition nwfs_Π_laws {C : category} (n : nwfs C) := pr2 (pr222 n).
Definition nwfs_R_monad {C : category} (n : nwfs C) := R_monad (nwfs_fact n) (nwfs_Π n) (nwfs_Π_laws n).
Definition nwfs_L_monad {C : category} (n : nwfs C) := L_monad (nwfs_fact n) (nwfs_Σ n) (nwfs_Σ_laws n).

Definition nwfs_R_maps {C : category} (n : nwfs C) :=
    MonadAlg (nwfs_R_monad n).
Definition nwfs_L_maps {C : category} (n : nwfs C) :=
    MonadAlg (nwfs_L_monad n).


Lemma nwfs_Σ_top_map_id {C : category} (n : nwfs C) (f : arrow C) :
    arrow_mor00 (nwfs_Σ n f) = identity _.
Proof.
  set (law1 := Monad_law1 (T:=nwfs_L_monad n) f).
  specialize (dirprod_pr1 (pathsdirprodweq (base_paths _ _ law1))) as top.
  apply pathsinv0.
  etrans.
  exact (pathsinv0 top).
  apply id_right.
Qed.

Lemma nwfs_Σ_bottom_map_inv {C : category} (n : nwfs C) (f : arrow C) :
    arrow_mor11 (nwfs_Σ n f) · arrow_mor (fact_R n (fact_L n f)) = identity _.
Proof.
  set (law1 := Monad_law1 (T:=nwfs_L_monad n) f).
  specialize (dirprod_pr2 (pathsdirprodweq (base_paths _ _ law1))) as bottom.
  exact bottom.
Qed.

Lemma nwfs_Σ_bottom_map_L_is_middle_map_of_Σ {C : category} (n : nwfs C) (f : arrow C) :
    (arrow_mor11 (nwfs_Σ n f)) · arrow_mor11 (nwfs_Σ n (fact_L n f)) =
    (arrow_mor11 (nwfs_Σ n f)) · three_mor11 (functor_on_morphisms n (nwfs_Σ n f)).
Proof.
  set (law3 := Monad_law3 (T:=nwfs_L_monad n) f).
  specialize (dirprod_pr2 (pathsdirprodweq (base_paths _ _ law3))) as bottom.
  apply pathsinv0.
  exact bottom.
Qed.

Lemma nwfs_Π_bottom_map_id {C : category} (n : nwfs C) (f : arrow C) :
    arrow_mor11 (nwfs_Π n f) = identity _.
Proof.
  set (law1 := Monad_law1 (T:=nwfs_R_monad n) f).
  specialize (dirprod_pr2 (pathsdirprodweq (base_paths _ _ law1))) as bottom.
  apply pathsinv0.
  etrans.
  exact (pathsinv0 bottom).
  apply id_left.
Qed.

Lemma nwfs_Π_top_map_inv {C : category} (n : nwfs C) (f : arrow C) :
    arrow_mor (fact_L n (fact_R n f)) · arrow_mor00 (nwfs_Π n f) = identity _.
Proof.
  set (law1 := Monad_law1 (T:=nwfs_R_monad n) f).
  specialize (dirprod_pr1 (pathsdirprodweq (base_paths _ _ law1))) as top.
  exact top.
Qed.

Lemma nwfs_Π_bottom_map_R_is_middle_map_of_Π {C : category} (n : nwfs C) (f : arrow C) :
    arrow_mor00 (nwfs_Π n (fact_R n f)) · arrow_mor00 (nwfs_Π n f) =
    three_mor11 (functor_on_morphisms n (nwfs_Π n f)) · arrow_mor00 (nwfs_Π n f).
Proof.
  set (law3 := Monad_law3 (T:=nwfs_R_monad n) f).
  specialize (dirprod_pr1 (pathsdirprodweq (base_paths _ _ law3))) as top.
  apply pathsinv0.
  exact top.
Qed.

Definition fact_mor {C : category} (F F' : functorial_factorization C) :=
    section_nat_trans_disp F F'.

Definition fact_mor_nt {C : category} {F F' : functorial_factorization C} (α : fact_mor F F') :=
    section_nat_trans α.
Coercion fact_mor_nt : fact_mor >-> nat_trans.

Lemma fact_mor_whisker_d1_is_id {C : category} {F F' : functorial_factorization C}
    (α : fact_mor F F') :
    post_whisker α face_map_1 = nat_trans_id (functor_identity _).
Proof.
  apply nat_trans_eq.
  - apply homset_property.
  - intro.     trivial.
Defined.

Definition nwfs_L_mor {C : category} {n n' : nwfs C}
    (α : fact_mor n n') : (nwfs_L_monad n') (nwfs_L_monad n) :=
  post_whisker (op_nt α) (functor_opp face_map_2).
Definition nwfs_R_mor {C : category} {n n' : nwfs C}
    (α : fact_mor n n') : (nwfs_R_monad n) (nwfs_R_monad n') :=
  post_whisker α face_map_0.

Definition nwfs_mor_axioms {C : category} (n n' : nwfs C) (α : fact_mor n n') :=
    Monad_Mor_laws (nwfs_L_mor α) × Monad_Mor_laws (nwfs_R_mor α).

Lemma isaprop_nwfs_mor_axioms {C : category} (n n' : nwfs C) (α : fact_mor n n') :
  isaprop (nwfs_mor_axioms n n' α).
Proof.
  apply isapropdirprod ; apply isaprop_Monad_Mor_laws.
Qed.

Definition nwfs_mor {C : category} (n n' : nwfs C) :=
     α : fact_mor n n', nwfs_mor_axioms n n' α.

Lemma isaset_nwfs_mor {C : category} (n n' : nwfs C) : isaset (nwfs_mor n n').
Proof.
  apply isaset_total2.
  - apply isaset_section_nat_trans_disp.
  - intro. apply isasetaprop, isaprop_nwfs_mor_axioms.
Defined.

Definition fact_mor_from_nwfs_mor {C : category} {n n' : nwfs C}
    (α : nwfs_mor n n') := pr1 α.
Coercion fact_mor_from_nwfs_mor : nwfs_mor >-> fact_mor.

Definition nwfs_L_monad_mor {C : category} {n n' : nwfs C}
    (α : nwfs_mor n n') : Monad_Mor (nwfs_L_monad n') (nwfs_L_monad n) :=
  (nwfs_L_mor α,, dirprod_pr1 (pr2 α)).
Definition nwfs_R_monad_mor {C : category} {n n' : nwfs C}
    (α : nwfs_mor n n') : Monad_Mor (nwfs_R_monad n) (nwfs_R_monad n') :=
  (nwfs_R_mor α,, dirprod_pr2 (pr2 α)).

Section NWFS_cat.

Context (C : category).

Definition nwfs_precategory_ob_mor : precategory_ob_mor.
Proof.
  use make_precategory_ob_mor.
  - exact (nwfs C).
  - intros n n'.
    exact (nwfs_mor n n').
Defined.

Definition fact_id_is_nwfs_mor (n : nwfs C) : nwfs_mor_axioms n n (section_nat_trans_id (nwfs_fact n)).
Proof.
  split.
  - assert (H : nwfs_L_mor (section_nat_trans_id (nwfs_fact n)) = nat_trans_id (nwfs_L_monad n)).
    {
      use nat_trans_eq; [apply homset_property|].
      intro.
      apply subtypePath; [intro; apply homset_property|].
      apply pathsdirprod; cbn; trivial.
    }
    rewrite H.
    apply identity_Monad_Mor_laws.
  - assert (H : nwfs_R_mor (section_nat_trans_id (nwfs_fact n)) = nat_trans_id (nwfs_R_monad n)).
    {
      use nat_trans_eq; [apply homset_property|].
      intro.
      apply subtypePath; [intro; apply homset_property|].
      apply pathsdirprod; cbn; trivial.
    }
    rewrite H.
    apply identity_Monad_Mor_laws.
Qed.

Definition nwfs_mor_id (n : nwfs C) : nwfs_mor n n.
Proof.
  use tpair.
  - exact (section_nat_trans_id (nwfs_fact n)).
  - exact (fact_id_is_nwfs_mor n).
Defined.

Definition nwfs_mor_comp (n n' n'' : nwfs C) :
    (nwfs_mor n n') -> (nwfs_mor n' n'') -> (nwfs_mor n n'').
Proof.
  intros α α'.

  use tpair.
  - exact (section_nat_trans_comp (fact_mor_from_nwfs_mor α) (fact_mor_from_nwfs_mor α')).
  - split.
    * assert (nwfs_L_mor (section_nat_trans_comp (pr1 α) (pr1 α')) =
              nat_trans_comp _ _ _ (nwfs_L_monad_mor α') (nwfs_L_monad_mor α)) as H.
      {
        simpl.
        use nat_trans_eq.
        -
          exact (homset_property (op_cat (arrow C))).
        - intro x; simpl in x.
          apply subtypePath; [intro; apply homset_property|].
          simpl.
          apply pathsdirprod; cbn.
          * now rewrite id_left.
          * unfold three_mor11.
            simpl.
            unfold mor_disp; simpl.
            rewrite pr1_transportf.
            rewrite transportf_const.
            trivial.
      }
      unfold fact_mor_from_nwfs_mor.
      rewrite H.
      exact (composition_Monad_Mor_laws (nwfs_L_monad_mor α') (nwfs_L_monad_mor α)).
    * assert (nwfs_R_mor (section_nat_trans_comp (pr1 α) (pr1 α')) =
              nat_trans_comp _ _ _ (nwfs_R_monad_mor α) (nwfs_R_monad_mor α')) as H.
      {
        simpl.
        use nat_trans_eq.
        -
          exact (homset_property (arrow C)).
        - intro x; simpl in x.
          apply subtypePath; [intro; apply homset_property|].
          simpl.
          apply pathsdirprod; cbn.
          * unfold three_mor11.
            simpl.
            unfold mor_disp; simpl.
            rewrite pr1_transportf.
            rewrite transportf_const.
            trivial.
          * now rewrite id_left.
      }
      unfold fact_mor_from_nwfs_mor.
      rewrite H.
      exact (composition_Monad_Mor_laws (nwfs_R_monad_mor α) (nwfs_R_monad_mor α')).
Defined.

Definition nwfs_precategory_data : precategory_data.
Proof.
  use make_precategory_data.
  - exact nwfs_precategory_ob_mor.
  - exact nwfs_mor_id.
  - exact nwfs_mor_comp.
Defined.

Definition nwfs_is_precategory : is_precategory nwfs_precategory_data.
Proof.
  use make_is_precategory_one_assoc; intros.
  - apply subtypePath; [intro; apply isaprop_nwfs_mor_axioms|cbn].
    apply section_nat_trans_id_left.
  - apply subtypePath; [intro; apply isaprop_nwfs_mor_axioms|cbn].
    apply section_nat_trans_id_right.
  - apply subtypePath; [intro; apply isaprop_nwfs_mor_axioms|cbn].
    apply section_nat_trans_assoc.
Qed.

Definition NWFS_precat : precategory :=
    (nwfs_precategory_data,, nwfs_is_precategory).

Lemma has_homsets_NWFS : has_homsets NWFS_precat.
Proof.
  intros n n' .
  use isaset_nwfs_mor.
Qed.

Definition NWFS : category := (NWFS_precat,, has_homsets_NWFS).

End NWFS_cat.