proposition: Lemma exponential_is_object : is_monoid_action exponential_object_data.
proof: Proof. use make_is_monoid_action; refine (λ (f : monoid_action_morphism _ _), _); intros; apply monoid_action_morphism_eq; intro; refine (maponpaths (λ x, f (x ,, _)) _). - apply unax. - 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