proposition: Lemma LNWFS_lcomp_comul_mul_law11 {F' F : Ff C} (L' : lnwfs_over F') (L : lnwfs_over F) (a : arrow C) : arrow_mor11 ( (disp_δ (L_monad_data (F' ⊗ F) (LNWFS_lcomp_comul L' L)) a) · (# (fact_L (F' ⊗ F)) (disp_δ (L_monad_data (F' ⊗ F) (LNWFS_lcomp_comul L' L)) a)) ) = arrow_mor11 ( (disp_δ (L_monad_data (F' ⊗ F) (LNWFS_lcomp_comul L' L)) a) · (disp_δ (L_monad_data (F' ⊗ F) (LNWFS_lcomp_comul L' L)) (fact_L (F' ⊗ F) a)) ).
proof: Proof. set (law3 := @Comonad_law3 _ (L_monad _ _ (pr2 L))). set (law3' := @Comonad_law3 _ (L_monad _ _ (pr2 L'))). apply pathsinv0. etrans. apply assoc'. etrans. apply cancel_precomposition, assoc. apply pathsinv0. etrans. apply assoc'. etrans. apply cancel_precomposition. { apply (pr1_section_disp_on_morphisms_comp F'). } set (natL'L'_lp := nat_trans_ax (pr1 L') _ _ (LNWFS_lcomp_comul_L'_lp L' L a)). apply pathsinv0. etrans. apply cancel_precomposition, cancel_postcomposition. exact (pr2 (pathsdirprodweq (base_paths _ _ (natL'L'_lp)))). etrans. apply assoc. etrans. apply cancel_postcomposition, assoc. etrans. apply assoc'. etrans. apply cancel_postcomposition. exact (pathsinv0 (pr2 (pathsdirprodweq (base_paths _ _ (law3' (fact_R F a)))))). etrans. apply assoc'. apply cancel_precomposition. etrans. apply cancel_precomposition. apply (pr1_section_disp_on_morphisms_comp F'). etrans. apply (pr1_section_disp_on_morphisms_comp F'). use (section_disp_on_eq_morphisms F'). - etrans. apply assoc. apply pathsinv0. etrans. apply assoc'. apply pathsinv0. etrans. do 2 apply cancel_postcomposition. exact (lnwfs_Σ_top_map_id L' (fact_R F a)). etrans. apply cancel_postcomposition, id_left. etrans. apply assoc'. set (natLL_lp := nat_trans_ax (pr1 L) _ _ (LNWFS_lcomp_comul_L_lp L F' a)). etrans. apply cancel_precomposition. apply assoc. etrans. apply cancel_precomposition, cancel_postcomposition. exact (pr2 (pathsdirprodweq (base_paths _ _ natLL_lp))). etrans. apply assoc. etrans. apply cancel_postcomposition, assoc. etrans. apply assoc'. etrans. apply cancel_postcomposition. exact (pathsinv0 (pr2 (pathsdirprodweq (base_paths _ _ (law3 a))))). etrans. apply assoc'. apply cancel_precomposition. etrans. apply cancel_precomposition. apply (pr1_section_disp_on_morphisms_comp F). etrans. apply (pr1_section_disp_on_morphisms_comp F). apply pathsinv0. etrans. apply (pr1_section_disp_on_morphisms_comp F). apply (section_disp_on_eq_morphisms F). * apply pathsinv0. etrans. apply cancel_postcomposition. exact (lnwfs_Σ_top_map_id L a). apply id_left. * etrans. apply assoc. etrans. apply cancel_postcomposition. { set (Σ'ρa := pr1 L' (fact_R F a)). etrans. exact (pathsinv0 (arrow_mor_comm Σ'ρa)). etrans. apply cancel_postcomposition. exact (lnwfs_Σ_top_map_id L' (fact_R F a)). apply id_left. } apply pathsinv0. etrans. apply assoc. exact (arrow_mor_comm (#(fact_L F') (LNWFS_lcomp_comul_L'_lp L' L a))). - etrans. apply cancel_precomposition. apply id_right. apply pathsinv0. apply id_left. 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