proposition: Lemma LNWFS_lcomp_comul_axioms {F' F : Ff C} (L' : lnwfs_over F') (L : lnwfs_over F) : is_nat_trans _ _ (LNWFS_lcomp_comul_data L' L).
proof: Proof. intros f g γ. use arrow_mor_eq; [etrans; [apply id_right|]; apply pathsinv0; apply id_left|]. etrans. { etrans. apply assoc. set (L'natργ := nat_trans_ax (pr1 L') _ _ (#(fact_R F) γ)). set (L'natργ11 := pr2 (pathsdirprodweq (base_paths _ _ L'natργ))). etrans. apply cancel_postcomposition. exact L'natργ11. etrans. apply assoc'. apply cancel_precomposition. use (pr1_section_disp_on_morphisms_comp F'). } apply pathsinv0. etrans. apply assoc'. apply cancel_precomposition. etrans. use (pr1_section_disp_on_morphisms_comp F'). use (section_disp_on_eq_morphisms F'); [|etrans; [apply id_left|]; apply pathsinv0; apply id_right]. apply pathsinv0. etrans. apply assoc. etrans. apply cancel_postcomposition. { set (Lnatγ := nat_trans_ax (pr1 L) _ _ γ). set (Lnatγ11 := pr2 (pathsdirprodweq (base_paths _ _ Lnatγ))). exact (Lnatγ11). } etrans. apply assoc'. apply pathsinv0. etrans. apply assoc'. apply cancel_precomposition. etrans. use (pr1_section_disp_on_morphisms_comp F). apply pathsinv0. etrans. use (pr1_section_disp_on_morphisms_comp F). use (section_disp_on_eq_morphisms F); [etrans; [apply id_right|]; apply pathsinv0; apply id_left|]. apply pathsinv0. exact (pr1 (three_mor_comm (#(fact_functor F') (#(fact_R F ) γ)))). Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Monads.Monads UniMath.CategoryTheory.Monads.Comonads UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.DisplayedCats.Examples.Arrow UniMath.CategoryTheory.DisplayedCats.Examples.Three UniMath.ModelCategories.Lifting UniMath.ModelCategories.NWFS UniMath.ModelCategories.Helpers UniMath.ModelCategories.Generated.LNWFSHelpers UniMath.ModelCategories.Generated.FFMonoidalStructure