Definition unit_monoid (V : monoidal_cat) : monoid V (monoidal_unit V). Proof. use make_monoid. - exact (monoidal_leftunitordata V (monoidal_unit V)). - exact (identity (monoidal_unit V)). - etrans. { apply maponpaths_2. apply (bifunctor_rightid V). } apply id_left. - etrans. { apply maponpaths_2. apply (bifunctor_leftid V). } refine (id_left _ @ _). apply unitors_coincide_on_unit. - apply maponpaths_2. etrans. 2: { rewrite unitors_coincide_on_unit. apply monoidal_triangleidentity. } apply idpath. 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.