proposition: Lemma Ff_monoid_is_RNWFS_mul_axioms {F : Ff C} (R : monoid (Ff_monoidal) F) : is_nat_trans _ _ (Ff_monoid_is_RNWFS_mul_data R).
proof: Proof. intros f f' γ. set (μ := monoid_data_multiplication _ R). set (μaxγ := (section_nt_disp_axioms_from_section_nt_disp μ) _ _ γ). set (μaxγb := base_paths _ _ μaxγ). apply subtypePath; [intro; apply homset_property|]. apply pathsdirprod. - apply pathsinv0. etrans. exact (pathsinv0 μaxγb). etrans. use pr1_transportf_const. apply cancel_postcomposition. use (section_disp_on_eq_morphisms F); reflexivity. - etrans. apply id_right. apply pathsinv0. etrans. apply id_left. reflexivity. 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.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.Combinatorics.StandardFiniteSets UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Graphs.Coequalizers UniMath.CategoryTheory.Chains.Chains UniMath.CategoryTheory.DisplayedCats.Examples.Arrow UniMath.CategoryTheory.DisplayedCats.Examples.Three UniMath.ModelCategories.NWFS UniMath.ModelCategories.Helpers UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monads.Monads UniMath.CategoryTheory.Monoidal.CategoriesOfMonoids