proposition: Lemma extension_functor_ob_is_monoid_action : is_monoid_action extension_functor_ob_monoid_action_data.
proof: Proof. use make_is_monoid_action. - intro x. use (issurjsetquotpr _ x (_ ,, isasetsetquot _ _ _) _). intro y. rewrite <- (pr2 y). refine (setquotfuncomm _ _ _ _ _ @ _). apply (maponpaths (λ x, _ (_ ,, x))). apply runax. - intros x m m'. use (issurjsetquotpr _ x (_ ,, isasetsetquot _ _ _) _). intro y. rewrite <- (pr2 y). refine (setquotfuncomm _ _ _ _ _ @ !_). refine (maponpaths _ (setquotfuncomm _ _ _ _ _) @ _). refine (setquotfuncomm _ _ _ _ _ @ !_). apply (maponpaths (λ x, _ (_ ,, x))). symmetry. apply assocax. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Algebra.Monoids UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.MonoEpiIso UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.exponentials UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.Preservation UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total