Library UniMath.ModelCategories.NWFS

Natural Weak Factorization Systems

Natural Weak Factorization Systems (NWFSs) are an algebraic refinement to WFSs. They consist of a functorial factorization, together with an extension of the left functor to a comonad and the right functor to a monad. These algebraic structures (note: NOT properties), make it so they behave better than WFSs, satisfying even those properties that required the axiom of choice for a WFS. In fact, one can construct a WFS from a NWFS in a canonical way (see ./NWFSisWFS.v).

The algebraic structure allows us to define categories out of functorial factorizations and NWFSs. It turns out to be useful to split this up into two halves: the left part of a NWFS (LNWFS) and the right part of a NWFS (RNWFS), consisting of the comonad and the monad extension respectively.

Important sources:

Cofibrantly generated natural weak factorisation systems by Richard Garner
Understanding the small object argument by Richard Garner
My thesis: https://studenttheses.uu.nl/handle/20.500.12932/45658
Natural weak factorization systems by Grandis and Tholen

Contents:

Preliminary definitions
Functorial Factorizations
LNWFS / RNWFS / NWFS definitions
NWFS properties
Definition of L- and R-Maps
Functorial factorization category
LNWFS category
RNWFS category
NWFS category
Some helper functions used in the formalization of the Algebraic Small Object Argument

face map 1 now rolls out just as the projection

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

we have to define face maps 0 and 2 as proper functors, since we need the factorization to obtain an object in the arrow category.

Definition face_map_0_data : functor_data (three C) (arrow C).
Show 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))
      ).

Definition face_map_0_axioms : is_functor face_map_0_data.
Show proof.

  split.
  -
    intro.
    apply subtypePath; [intro; apply homset_property|].
    reflexivity.
  -
    intros a b c f g.
    apply subtypePath; [intro; apply homset_property|].
    reflexivity.

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

Definition face_map_2_data : functor_data (three C) (arrow C).
Show 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)))
      ).

Definition face_map_2_axioms : is_functor face_map_2_data.
Show proof.

  split.
  -
    intro.
    apply subtypePath; [intro; apply homset_property|].
    trivial.
  -
    intros a b c f g.
    apply subtypePath; [intro; apply homset_property|].
    trivial.

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

verify that they are indeed compatible

Lemma face_compatibility (fg : three C) :
arrow_mor (face_map_2 fg) · arrow_mor (face_map_0 fg)
= arrow_mor (face_map_1 fg).
Show proof.

exact (three_comp fg).

this natural transformation boils down to square

  0 ===== 0
  |       |
  |       |
  1 ----> 2

Definition c_21_data : nat_trans_data face_map_2 face_map_1.
Show proof.

  intro xxx.
  simpl.
  exists (make_dirprod (identity _) (three_mor12 xxx)).
  abstract (
    simpl;
    rewrite id_left;
    apply pathsinv0;
    exact (three_comp xxx)
  ).

Definition c_21_axioms : is_nat_trans _ _ c_21_data.
Show 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)).

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

this natural transformation boils down to square

  0 ----> 1
  |       |
  |       |
  2 ===== 2

Definition c_10_data : nat_trans_data face_map_1 face_map_0.
Show proof.

  intro xxx.
  exists (make_dirprod (three_mor01 xxx) (identity _)).
  abstract (
    simpl;
    rewrite id_right;
    exact (three_comp xxx)
  ).

Definition c_10_axioms : is_nat_trans _ _ c_10_data.
Show 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.

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 {_}.

We can't really do this with the "naive definition" of three C, since then we need the middle object for the section. We would have to define our own theory.

Definition functorial_factorization (C : category) := section_disp (three_disp C).
#[reversible] 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.

Functorial factorizations indeed split face map 1 (d1)

Lemma functorial_factorization_splits_face_map_1 {C : category} (F : functorial_factorization C) :
F ∙ face_map_1 = functor_identity (arrow C).
Show proof.

apply functor_eq; trivial.
apply homset_property.

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.

At least now it knows they are compatible

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

intro.
exact (three_comp _).

  exists F.
  split.
  - exists Σ. exact L.
  - exists Π. exact R.

the following lemmas about Σ and Π are from Grandis, Tholen, (6), (7), diagram after (7), (8), (9) diagram after (7)

Lemma nwfs_Σ_top_map_id {C : category} (n : nwfs C) (f : arrow C) :
arrow_mor00 (nwfs_Σ n f) = identity _.
Show 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.

σf · ρ_{λf} = id (6, 2nd)

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 _.
Show proof.
  set (law1 := Comonad_law1 (T:=nwfs_L_monad n) f).
  set (bottom := arrow_mor11_eq law1).
  exact bottom.

σf · σ_{λf} = σf · F(1_A, σf) where F(1_a, σf) is the map on middle objects of F(Σf) if we see Σf as a morphism in the arrow category (9, top right + cancel_postcomposition)

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)).
Show proof.
  set (law3 := Comonad_law3 (T:=nwfs_L_monad n) f).
  set (bottom := arrow_mor11_eq law3).
  apply pathsinv0.
  exact bottom.

diagram after (7)

Lemma nwfs_Π_bottom_map_id {C : category} (n : nwfs C) (f : arrow C) :
    arrow_mor11 (nwfs_Π n f) = identity _.
Show 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.

λ_{ρf} · πf = id (6, 4th)

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 _.
Show proof.
  set (law1 := Monad_law1 (T:=nwfs_R_monad n) f).
  set (top := arrow_mor00_eq law1).
  exact top.

π_{ρf} · πf = F(πf, 1_b) · πf) where F(πf, 1_b) = map on middle objects of F(Πf) if we see Πf as a morphism in the arrow category (9, bottom right + cancel_precomposition)

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).
Show proof.
  set (law3 := Monad_law3 (T:=nwfs_R_monad n) f).
  set (top := arrow_mor00_eq law3).
  apply pathsinv0.
  exact top.

L-Map AND R-Map FOR AN NWFS n

In a monad algebra, we have [f αf] laws : nwfs_R_maps n

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

Shape of comonad morphism diagram (2.15, Garner)
A ===== A ===== A ~~> id_A | | | f | α |λf η | f v v v B ---> Kf ----> B ~~> id_B s ρ_f

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

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 _.
Show proof.
  exists (pr211 hf).
  apply R_map_section_comm.

Shape of monad morphism diagram (2.15, Garner)
λg p C ---> Kg ----> C ~~> id_C | | | g | η |ρg α | g v v v D ===== D ===== D ~~> id_D

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

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 _.
Show proof.
  exists (pr111 hg).
  apply L_map_retraction_comm.

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.
Show 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
    ]
  ).

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').
Show proof.
  apply isaset_section_nat_trans_disp.

verify that indeed, whiskering with d1 yields id{C^2} ⟹ id{C^2}

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 _).
Show proof.
  apply nat_trans_eq.
  - apply homset_property.
  - intro.     trivial.

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

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'').
Show proof.
  intros τ τ'.
  exact (section_nat_trans_comp τ τ').

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

Definition Ff_is_precategory (C : category) : is_precategory (Ff_precategory_data C).
Show 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.

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

Definition has_homsets_Ff (C : category) : has_homsets (Ff_precategory C).
Show proof.
  intros F F'.
  use isaset_fact_mor.

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' τ).
Show proof.
  apply isaprop_disp_Comonad_Mor_laws.

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' τ).
Show proof.
  apply isaprop_disp_Monad_Mor_laws.

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' τ).
Show proof.
  apply isapropdirprod.
  - apply isaprop_lnwfs_mor_axioms.
  - apply isaprop_rnwfs_mor_axioms.

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

We just show that fact_id corresponds with the identity monad morphisms on L and R.

Lemma fact_id_is_lnwfs_mor {F : functorial_factorization C} (n : lnwfs_over F) : lnwfs_mor_axioms n n (Ff_precategory_id F).
Show 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)).

Lemma fact_id_is_rnwfs_mor {F : functorial_factorization C} (n : rnwfs_over F) : rnwfs_mor_axioms n n (Ff_precategory_id F).
Show 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)).

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'' (τ · τ').
Show 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'
  ).

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'' (τ · τ').
Show 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'
  ).

Definition LNWFS : disp_cat (Ff C).
Show 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').

Definition RNWFS : disp_cat (Ff C).
Show 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').

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.
Show proof.
  now induction H.

the above equality, but on the middle morphisms

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).
Show proof.
  now induction H.

specific version of the above that we need in a proof

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).
Show proof.
  induction H.
  intro f.
  apply pathsinv0.
  etrans. apply pr1_transportf_const.
  reflexivity.

End Helpers.