Library UniMath.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.Comonads.
Require Import UniMath.CategoryTheory.Monads.MonadAlgebras.
Require Import UniMath.CategoryTheory.Monads.ComonadCoalgebras.

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

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

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)).
    * exact (three_mor12 xxx).
  - intros xxx yyy fff.
    use mors_to_arrow_mor.
    * exact (three_mor11 fff).
    * exact (three_mor22 fff).
    *
      abstract (
        apply pathsinv0;
        exact (pr2 (three_mor_comm fff))
      ).
Defined.

Definition face_map_0_axioms : is_functor face_map_0_data.
Proof.
  split.
  -
    intro.
    apply subtypePath; [intro; apply homset_property|].
    reflexivity.
  -
    intros a b c f g.
    apply subtypePath; [intro; apply homset_property|].
    reflexivity.
Qed.

Definition face_map_0 : three C ⟶ arrow C :=
    (_,, face_map_0_axioms).

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.
    use mors_to_arrow_mor.
    * exact (three_mor00 fff).
    * exact (three_mor11 fff).
    * abstract (
        exact (pathsinv0 (pr1 (three_mor_comm fff)))
      ).
Defined.

Definition face_map_2_axioms : is_functor face_map_2_data.
Proof.
  split.
  -
    intro.
    apply subtypePath; [intro; apply homset_property|].
    trivial.
  -
    intros a b c f g.
    apply subtypePath; [intro; apply homset_property|].
    trivial.
Qed.

Definition face_map_2 : three C ⟶ arrow C :=
    (_,, face_map_2_axioms).

Lemma face_compatibility (fg : three C) :
    arrow_mor (face_map_2 fg) · arrow_mor (face_map_0 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)).
  abstract (
    simpl;
    rewrite id_left;
    apply pathsinv0;
    exact (three_comp xxx)
  ).
Defined.

Definition c_21_axioms : is_nat_trans _ _ c_21_data.
Proof.
  intros xxx yyy ff.

  apply subtypePath.
  *
    intro.
    apply homset_property.
  *
    apply pathsdirprod.
    + etrans. apply id_right.
      apply pathsinv0.
      apply id_left.
    + apply pathsinv0.
      exact (pr2 (three_mor_comm ff)).
Qed.

Definition c_21 : face_map_2 ⟹ face_map_1 :=
    (_,, c_21_axioms).

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

Definition c_10_axioms : is_nat_trans _ _ c_10_data.
Proof.
  intros xxx yyy ff.
  apply subtypePath.
  - intro x.
    apply homset_property.
  - apply pathsdirprod.
    * apply pathsinv0.
      exact (pr1 (three_mor_comm ff)).
    * etrans. apply id_right.
      apply pathsinv0.
      apply id_left.
Qed.

Definition c_10 : face_map_1 ⟹ face_map_0 :=
    (_,, c_10_axioms).

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).
Coercion 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.
Qed.

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 _).
Qed.

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) :=
  make_dirprod Π (Λ 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) :=
  (_,, 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_Comonad_data (fact_L F) :=
  make_dirprod Σ (Φ F).

Definition L_monad {C : category} (F : functorial_factorization C)
    (Σ : (fact_L F) ⟹ (fact_L F) ∙ (fact_L F))
    (L : disp_Comonad_laws (L_monad_data F Σ)) : Comonad (arrow C) :=
  (_,, L_monad_data F Σ,, L).

Definition lnwfs_over {C : category} (F : functorial_factorization C) :=
    ∑ (Σ : (fact_L F) ⟹ (fact_L F) ∙ (fact_L F)), disp_Comonad_laws (L_monad_data F Σ).

Definition rnwfs_over {C : category} (F : functorial_factorization C) :=
    ∑ (Π : (fact_R F) ∙ (fact_R F) ⟹ (fact_R F)), disp_Monad_laws (R_monad_data F Π).

Definition nwfs_over {C : category} (F : functorial_factorization C) :=
    (lnwfs_over F) × (rnwfs_over F).

Definition nwfs (C : category) :=
    ∑ (F : functorial_factorization C), nwfs_over F.

Definition nwfs_over_to_nwfs {C : category} {F : functorial_factorization C} (n : nwfs_over F) : nwfs C :=
    (_,, n).
Coercion nwfs_over_to_nwfs : nwfs_over >-> nwfs.
Definition nwfs_over_to_fact {C : category} {F : functorial_factorization C} (n : nwfs_over F) : functorial_factorization C :=
    F.
Coercion nwfs_over_to_fact : nwfs_over >-> functorial_factorization.

Definition make_nwfs {C : category} (F : functorial_factorization C)
    (Σ : (fact_L F) ⟹ (fact_L F) ∙ (fact_L F)) (L : disp_Comonad_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.
  split.
  - exists Σ. exact L.
  - exists Π. exact R.
Defined.

Definition nwfs_fact {C : category} (n : nwfs C) := pr1 n.
Coercion nwfs_fact : nwfs >-> functorial_factorization.
Definition nwfs_lnwfs {C : category} (n : nwfs C) := pr12 n.
Coercion nwfs_lnwfs : nwfs >-> lnwfs_over.
Definition nwfs_rnwfs {C : category} (n : nwfs C) := pr22 n.
Coercion nwfs_rnwfs : nwfs >-> rnwfs_over.
Definition nwfs_Σ {C : category} (n : nwfs C) := pr1 (nwfs_lnwfs n).
Definition nwfs_Π {C : category} (n : nwfs C) := pr1 (nwfs_rnwfs n).
Definition nwfs_Σ_laws {C : category} (n : nwfs C) := pr2 (nwfs_lnwfs n).
Definition nwfs_Π_laws {C : category} (n : nwfs C) := pr2 (nwfs_rnwfs n).
Definition rnwfs_R_monad {C : category} {F : functorial_factorization C} (n : rnwfs_over F) := R_monad F (pr1 n) (pr2 n).
Definition rnwfs_R_monad_data {C : category} {F : functorial_factorization C} (n : rnwfs_over F) := pr12 (R_monad F (pr1 n) (pr2 n)).
Definition lnwfs_L_monad {C : category} {F : functorial_factorization C} (n : lnwfs_over F) := L_monad F (pr1 n) (pr2 n).
Definition lnwfs_L_monad_data {C : category} {F : functorial_factorization C} (n : lnwfs_over F) := pr12 (L_monad F (pr1 n) (pr2 n)).
Definition nwfs_R_monad {C : category} (n : nwfs C) := rnwfs_R_monad (nwfs_rnwfs n).
Definition nwfs_L_monad {C : category} (n : nwfs C) := lnwfs_L_monad (nwfs_lnwfs n).

Lemma nwfs_Σ_top_map_id {C : category} (n : nwfs C) (f : arrow C) :
    arrow_mor00 (nwfs_Σ n f) = identity _.
Proof.
  set (law1 := Comonad_law1 (T:=nwfs_L_monad n) f).
  set (top := arrow_mor00_eq law1).
  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 := Comonad_law1 (T:=nwfs_L_monad n) f).
  set (bottom := arrow_mor11_eq law1).
  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 := Comonad_law3 (T:=nwfs_L_monad n) f).
  set (bottom := arrow_mor11_eq law3).
  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).
  set (bottom := arrow_mor11_eq law1).
  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).
  set (top := arrow_mor00_eq law1).
  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).
  set (top := arrow_mor00_eq law3).
  apply pathsinv0.
  exact top.
Qed.


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

Lemma R_map_section_comm {C : category} {n : nwfs C} {a b : C} {f : a --> b}
    (hf : nwfs_L_maps n f) (s := pr211 hf) :
  f · s = arrow_mor (fact_L n f) ×
     s · arrow_mor (fact_R n f) = identity _.
Proof.
  set (ida := pr111 hf).
  set (αfcomm := pr21 hf).
  set (hαfη := pr12 hf).

  cbn in ida, s, αfcomm.
  simpl in hαfη.

  assert (ida = identity a) as Hida.
  {
    
    set (top_line := dirprod_pr1 (pathsdirprodweq (base_paths _ _ hαfη))).
    rewrite id_right in top_line.
    exact top_line.
  }

  split.
  -
    
    specialize (αfcomm) as αfcomm'.
    unfold ida in Hida.
    rewrite Hida, id_left in αfcomm'.
    apply pathsinv0.
    exact αfcomm'.
  -
    
    set (bottom_line := dirprod_pr2 (pathsdirprodweq (base_paths _ _ hαfη))).
    exact bottom_line.
Qed.

Lemma R_map_section {C : category} {n : nwfs C} {a b : C} {f : a --> b}
    (hf : nwfs_L_maps n f) :
  ∑ s, f · s = arrow_mor (fact_L n f) ×
      s · arrow_mor (fact_R n f) = identity _.
Proof.
  exists (pr211 hf).
  apply R_map_section_comm.
Defined.

Lemma L_map_retraction_comm {C : category} {n : nwfs C} {c d : C} {g : c --> d}
    (hg : nwfs_R_maps n g) (p := pr111 hg) :
  p · g = arrow_mor (fact_R n g) ×
      arrow_mor (fact_L n g) · p = identity _.
Proof.
  set (idd := pr211 hg).
  set (αgcomm := pr21 hg).
  set (hαgη := pr12 hg).

  cbn in p, idd, αgcomm.
  simpl in hαgη.

  assert (idd = identity d) as Hidd.
  {
    
    set (bottom_line := dirprod_pr2 (pathsdirprodweq (base_paths _ _ hαgη))).
    rewrite id_left in bottom_line.
    exact bottom_line.
  }

  split.
  -
    
    specialize (αgcomm) as αgcomm'.
    unfold idd in Hidd.
    rewrite Hidd, id_right in αgcomm'.
    exact αgcomm'.
  -
    
    set (top_line := dirprod_pr1 (pathsdirprodweq (base_paths _ _ hαgη))).
    exact top_line.
Qed.

Lemma L_map_retraction {C : category} {n : nwfs C} {c d : C} {g : c --> d}
    (hg : nwfs_R_maps n g) :
  ∑ p, p · g = arrow_mor (fact_R n g) ×
      arrow_mor (fact_L n g) · p = identity _.
Proof.
  exists (pr111 hg).
  apply L_map_retraction_comm.
Defined.

Lemma L_map_R_map_elp {C : category} {n : nwfs C} {a b c d : C}
    {f : a --> b} {g : c --> d} (hf : nwfs_L_maps n f)
    (hg : nwfs_R_maps n g) : elp f g.
Proof.
  intros h k H.

  destruct (R_map_section hf) as [s [Hs0 Hs1]].
  destruct (L_map_retraction hg) as [p [Hp0 Hp1]].

  set (hk := mors_to_arrow_mor f g h k H).
  set (Fhk := functor_on_morphisms (fact_functor n) hk).
  set (Khk := three_mor11 Fhk).

  set (Hhk := three_mor_comm Fhk).
  simpl in Hhk.
  destruct Hhk as [Hhk0 Hhk1].


  exists (s · Khk · p).

  abstract (
    split; [
      
      rewrite assoc, assoc;
      rewrite Hs0;
      
      
      etrans; [apply maponpaths_2;
               exact Hhk0|];
      
      
      rewrite <- assoc;
      etrans; [apply maponpaths;
               exact Hp1|];
      
      now rewrite id_right
    |
      rewrite <- (assoc _ p g);
      rewrite Hp0;
      
      
      rewrite <- assoc;
      etrans; [apply maponpaths;
               exact (pathsinv0 Hhk1)|];
      
      
      rewrite assoc;
      etrans; [apply maponpaths_2;
               exact Hs1|];
      
      now rewrite id_left
    ]
  ).
Defined.


Section NWFS_cat.

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 isaset_fact_mor {C : category} (F F' : functorial_factorization C) : isaset (fact_mor F F').
Proof.
  apply isaset_section_nat_trans_disp.
Qed.

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

Definition Ff_precategory_ob_mor (C : category) : precategory_ob_mor.
Proof.
  use make_precategory_ob_mor.
  - exact (functorial_factorization C).
  - intros F F'.
    exact (fact_mor F F').
Defined.

Definition Ff_precategory_id {C : category} (F : functorial_factorization C) : fact_mor F F :=
    section_nat_trans_id F.

Definition Ff_precategory_comp {C : category} (F F' F'' : functorial_factorization C) :
    (fact_mor F F') -> (fact_mor F' F'') -> (fact_mor F F'').
Proof.
  intros τ τ'.
  exact (section_nat_trans_comp τ τ').
Defined.

Definition Ff_precategory_data (C : category) : precategory_data.
Proof.
  use make_precategory_data.
  - exact (Ff_precategory_ob_mor C).
  - exact Ff_precategory_id.
  - exact Ff_precategory_comp.
Defined.

Definition Ff_is_precategory (C : category) : is_precategory (Ff_precategory_data C).
Proof.
  use make_is_precategory_one_assoc; intros.
  - apply section_nat_trans_id_left.
  - apply section_nat_trans_id_right.
  - apply section_nat_trans_assoc.
Qed.

Definition Ff_precategory (C : category) : precategory := (_,, Ff_is_precategory C).

Definition has_homsets_Ff (C : category) : has_homsets (Ff_precategory C).
Proof.
  intros F F'.
  use isaset_fact_mor.
Qed.

Definition Ff (C : category) : category := (Ff_precategory C,, has_homsets_Ff C).

Definition lnwfs_mor {C : category} {F F' : functorial_factorization C}
    (n : lnwfs_over F) (n' : lnwfs_over F')
    (τ : fact_mor F F') : (lnwfs_L_monad n) ⟹ (lnwfs_L_monad n') :=
  post_whisker (τ) (face_map_2).

Definition rnwfs_mor {C : category} {F F' : functorial_factorization C}
    (n : rnwfs_over F) (n' : rnwfs_over F')
    (τ : fact_mor F F') : (rnwfs_R_monad n) ⟹ (rnwfs_R_monad n') :=
  post_whisker τ face_map_0.

Definition lnwfs_mor_axioms {C : category} {F F' : functorial_factorization C}
    (n : lnwfs_over F) (n' : lnwfs_over F')
    (τ : fact_mor F F') :=
  disp_Comonad_Mor_laws (lnwfs_L_monad_data n) (lnwfs_L_monad_data n') (lnwfs_mor n n' τ).

Lemma isaprop_lnwfs_mor_axioms {C : category} {F F' : functorial_factorization C}
    (n : lnwfs_over F) (n' : lnwfs_over F')
    (τ : fact_mor F F') :
  isaprop (lnwfs_mor_axioms n n' τ).
Proof.
  apply isaprop_disp_Comonad_Mor_laws.
Qed.

Definition rnwfs_mor_axioms {C : category} {F F' : functorial_factorization C}
    (n : rnwfs_over F) (n' : rnwfs_over F')
    (τ : fact_mor F F') :=
  disp_Monad_Mor_laws (rnwfs_R_monad_data n) (rnwfs_R_monad_data n') (rnwfs_mor n n' τ).

Lemma isaprop_rnwfs_mor_axioms {C : category} {F F' : functorial_factorization C}
    (n : rnwfs_over F) (n' : rnwfs_over F')
    (τ : fact_mor F F') :
  isaprop (rnwfs_mor_axioms n n' τ).
Proof.
  apply isaprop_disp_Monad_Mor_laws.
Qed.

Definition nwfs_mor_axioms {C : category} (n n' : nwfs C) (τ : fact_mor n n') :=
    lnwfs_mor_axioms n n' τ × rnwfs_mor_axioms n n' τ.

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_lnwfs_mor_axioms.
  - apply isaprop_rnwfs_mor_axioms.
Qed.

Definition lnwfs_L_monad_mor {C : category}
    {F F' : functorial_factorization C}
    {n : lnwfs_over F}
    {n' : lnwfs_over F'}
    (τ : fact_mor F F')
    (ax : lnwfs_mor_axioms n n' τ) :
      Comonad_Mor (lnwfs_L_monad n) (lnwfs_L_monad n') :=
  (lnwfs_mor n n' τ,, ax).

Definition rnwfs_R_monad_mor {C : category}
    {F F' : functorial_factorization C}
    {n : rnwfs_over F}
    {n' : rnwfs_over F'}
    (τ : fact_mor F F')
    (ax : rnwfs_mor_axioms n n' τ) :
      Monad_Mor (rnwfs_R_monad n) (rnwfs_R_monad n') :=
  (rnwfs_mor n n' τ,, ax).

Context (C : category).

Lemma fact_id_is_lnwfs_mor {F : functorial_factorization C} (n : lnwfs_over F) : lnwfs_mor_axioms n n (Ff_precategory_id F).
Proof.
  assert (H : lnwfs_mor _ _ (Ff_precategory_id F) = nat_trans_id (lnwfs_L_monad n)).
  {
    use nat_trans_eq; [apply homset_property|].
    intro.
    apply subtypePath; [intro; apply homset_property|].
    apply pathsdirprod; reflexivity.
  }
  unfold lnwfs_mor_axioms.
  rewrite H.
  exact (comonads_category_id_subproof _ (pr2 n)).
Qed.

Lemma fact_id_is_rnwfs_mor {F : functorial_factorization C} (n : rnwfs_over F) : rnwfs_mor_axioms n n (Ff_precategory_id F).
Proof.
  assert (H : rnwfs_mor _ _ (Ff_precategory_id F) = nat_trans_id (rnwfs_R_monad n)).
  {
    use nat_trans_eq; [apply homset_property|].
    intro.
    apply subtypePath; [intro; apply homset_property|].
    apply pathsdirprod; cbn; trivial.
  }
  unfold rnwfs_mor_axioms.
  rewrite H.
  exact (monads_category_id_subproof _ (pr2 n)).
Qed.


Lemma lnwfs_mor_comp {F F' F'' : Ff C}
    {n : lnwfs_over F}
    {n' : lnwfs_over F'}
    {n'' : lnwfs_over F''}
    {τ : F --> F'}
    {τ' : F' --> F''}
    (ax : lnwfs_mor_axioms n n' τ)
    (ax' : lnwfs_mor_axioms n' n'' τ') :
  lnwfs_mor_axioms n n'' (τ · τ').
Proof.
  assert (lnwfs_mor n n'' (τ · τ') =
          nat_trans_comp _ _ _ (lnwfs_L_monad_mor τ ax) (lnwfs_L_monad_mor τ' ax')) as H.
  {
    use nat_trans_eq.
    -
      exact (homset_property (arrow C)).
    - intro x.
      use arrow_mor_eq.
      * apply pathsinv0.
        apply id_left.
      * etrans. use pr1_transportf_const.
        reflexivity.
  }
  unfold lnwfs_mor_axioms.
  rewrite H.
  exact (
    comonads_category_comp_subproof
      (lnwfs_L_monad_data n)
      (pr22 (lnwfs_L_monad n))
      (lnwfs_L_monad_data n')
      (pr22 (lnwfs_L_monad n'))
      (lnwfs_L_monad_data n'')
      (pr22 (lnwfs_L_monad n''))
      (lnwfs_L_monad_mor τ ax)
      (lnwfs_L_monad_mor τ' ax')
      ax ax'
  ).
Qed.

Lemma rnwfs_mor_comp {F F' F'' : Ff C}
    {n : rnwfs_over F}
    {n' : rnwfs_over F'}
    {n'' : rnwfs_over F''}
    {τ : F --> F'}
    {τ' : F' --> F''}
    (ax : rnwfs_mor_axioms n n' τ)
    (ax' : rnwfs_mor_axioms n' n'' τ') :
  rnwfs_mor_axioms n n'' (τ · τ').
Proof.
  assert (rnwfs_mor n n'' (τ · τ') =
          nat_trans_comp _ _ _ (rnwfs_R_monad_mor τ ax) (rnwfs_R_monad_mor τ' ax')) as H.
  {
    use nat_trans_eq.
    -
      exact (homset_property (arrow C)).
    - intro x; simpl in x.
      apply subtypePath; [intro; apply homset_property|].
      simpl.
      apply pathsdirprod; cbn.
      * etrans. use pr1_transportf_const.
        reflexivity.
      * now rewrite id_left.
  }
  unfold rnwfs_mor_axioms.
  rewrite H.

  exact (
    monads_category_comp_subproof
      (rnwfs_R_monad_data n)
      (pr22 (rnwfs_R_monad n))
      (rnwfs_R_monad_data n')
      (pr22 (rnwfs_R_monad n'))
      (rnwfs_R_monad_data n'')
      (pr22 (rnwfs_R_monad n''))
      (rnwfs_R_monad_mor τ ax)
      (rnwfs_R_monad_mor τ' ax')
      ax ax'
  ).
Qed.

Definition LNWFS : disp_cat (Ff C).
Proof.
  use disp_cat_from_SIP_data.
  - exact lnwfs_over.
  - exact (@lnwfs_mor_axioms C).
  - intros.
    apply isaprop_lnwfs_mor_axioms.
  - intros.
    apply fact_id_is_lnwfs_mor.
  - intros F F' F'' n n' n'' τ τ' ax ax'.
    apply (lnwfs_mor_comp ax ax').
Defined.

Definition RNWFS : disp_cat (Ff C).
Proof.
  use disp_cat_from_SIP_data.
  - exact rnwfs_over.
  - exact (@rnwfs_mor_axioms C).
  - intros.
    apply isaprop_rnwfs_mor_axioms.
  - intros.
    apply fact_id_is_rnwfs_mor.
  - intros F F' F'' n n' n'' τ τ' ax ax'.
    apply (rnwfs_mor_comp ax ax').
Defined.

Definition NWFS : disp_cat (Ff C) :=
    dirprod_disp_cat LNWFS RNWFS.

End NWFS_cat.

Section Helpers.

Lemma eq_section_nat_trans_component
    {C : category}
    {F F' : Ff C}
    {γ γ' : F --> F'}
    (H : γ = γ') :
  ∏ f, section_nat_trans γ f = section_nat_trans γ' f.
Proof.
  now induction H.
Qed.

Lemma eq_section_nat_trans_component11
    {C : category}
    {F F' : Ff C}
    {γ γ' : F --> F'}
    (H : γ = γ') :
  ∏ f, three_mor11 (section_nat_trans γ f) = three_mor11 (section_nat_trans γ' f).
Proof.
  now induction H.
Qed.

Lemma eq_section_nat_trans_comp_component11
    {C : category}
    {F F' F'' : Ff C}
    {γ : F --> F''}
    {γ' : F --> F'}
    {γ'' : F' --> F''}
    (H : γ' · γ'' = γ) :
  ∏ f,
    three_mor11 (section_nat_trans γ' f)
    · three_mor11 (section_nat_trans γ'' f)
    = three_mor11 (section_nat_trans γ f).
Proof.
  induction H.
  intro f.
  apply pathsinv0.
  etrans. apply pr1_transportf_const.
  reflexivity.
Qed.

End Helpers.