Definition is_monoid_ob (X : Mon) (μ : X ⊗ X --> X) (η : I --> X) : UU := (μ #⊗ id X · μ = pr1 α' ((X, X), X) · id X #⊗ μ · μ) × (pr1 λ' X = η #⊗ id X · μ) × (pr1 ρ' X = id X #⊗ η · μ).
Require Import UniMath.Foundations.PartD. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored.