proposition: Lemma exponential_object_is_morphism : ∏ x m, mor_action_ax exponential_object_morphism_data x m.
proof: Proof. intros x m. refine (_ @ mor_action _ _ _). apply (maponpaths (λ y, (pr2 x : monoid_action_morphism _ _) (y ,, _))). exact (runax _ _ @ !lunax _ _). 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