Definition monoid_presheaf_to_action : PreShv (monoid_to_category_ob M) ⟶ monoid_action_cat M. Proof. use make_functor. - use make_functor_data. + intro P. use make_monoid_action. * use make_monoid_action_data. -- exact ((P : _ ⟶ _) tt). -- intros p m. exact (# (P : _ ⟶ _) m p). * use make_is_monoid_action. -- intro x. exact (eqtohomot (functor_id P _) _). -- intros x m m'. exact (eqtohomot (functor_comp P m m') _). + intros P P' F. use make_monoid_action_morphism. * exact ((F : _ ⟹ _) tt). * intros x m. apply (eqtohomot (nat_trans_ax F _ _ _)). - abstract now split; repeat intro; apply monoid_action_morphism_eq. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.CategoryTheory.Categories.HSET.Univalence. Require Import UniMath.CategoryTheory.Categories.Monoid. Require Import UniMath.CategoryTheory.Categories.CategoryOfSetCategories. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Core.Setcategories. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Presheaf. Require Import UniMath.AlgebraicTheories.FundamentalTheorem.CommonUtilities.MonoidActions.