Definition make_monoid {x : C} (μ : C⟦x ⊗ x, x⟧) (η : C⟦monoidal_unit M, x⟧) (p_ul : (η ⊗r x) · μ = lu x) (p_ur : (x ⊗l η) · μ = ru x) (p_assoc : α x x x · (x ⊗l μ) · μ = μ ⊗r x · μ) : monoid x. Proof. simple refine ((_ ,, _) ,, (_ ,, _ ,, _)). - exact μ. - exact η. - exact p_ul. - exact p_ur. - exact p_assoc. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Import BifunctorNotations. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total.