proposition: Lemma Ff_monoid_is_RNWFS_monad_laws {F : Ff C} (R : monoid (Ff_monoidal) F) : disp_Monad_laws (R_monad_data F (Ff_monoid_is_RNWFS_mul R)).
proof: Proof. set (μ := monoid_data_multiplication _ R). repeat split. - intro f. apply subtypePath; [intro; apply homset_property|]. apply pathsdirprod; [|apply id_left]. set (μax := monoid_to_unit_left_law _ R). set (μf := (section_nat_trans_data_from_section_nat_trans_disp_funclass μ) f). set (μaxf := eq_section_nat_trans_disp_on_morphism μax f). set (μaxfb := base_paths _ _ μaxf). apply pathsinv0. etrans. exact (pathsinv0 μaxfb). etrans. use pr1_transportf_const. apply cancel_postcomposition. rewrite (Ff_point_unique _). reflexivity. - intro f. apply subtypePath; [intro; apply homset_property|]. apply pathsdirprod; [|apply id_left]. set (μax := monoid_to_unit_right_law _ R). set (μf := (section_nat_trans_data_from_section_nat_trans_disp_funclass μ) f). set (μaxf := eq_section_nat_trans_disp_on_morphism μax f). set (μaxfb := base_paths _ _ μaxf). apply pathsinv0. etrans. exact (pathsinv0 μaxfb). etrans. use pr1_transportf_const. apply cancel_postcomposition. rewrite (Ff_point_unique (monoid_data_unit Ff_monoidal R)). apply pathsinv0. etrans. apply (section_disp_on_eq_morphisms F (γ' := three_mor_mor12 (section_nat_trans (Ff_l_point F) f))); reflexivity. reflexivity. - intro f. apply subtypePath; [intro; apply homset_property|]. apply pathsdirprod; [|reflexivity]. set (μax := monoid_to_assoc_law _ R). set (μf := (section_nat_trans_data_from_section_nat_trans_disp_funclass μ) f). set (μaxf := eq_section_nat_trans_disp_on_morphism μax f). set (μaxfb := base_paths _ _ μaxf). use (pathscomp1 μaxfb). * etrans. use pr1_transportf_const. apply cancel_postcomposition. etrans. use pr1_transportf_const. etrans. apply id_left. reflexivity. * etrans. use pr1_transportf_const. apply cancel_postcomposition. 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