Definition constantly_unit_functor_fmonoidal : fmonoidal V V (constant_functor _ _ (I_{V})). Proof. use constant_functor_fmonoidal. - apply unit_monoid. - exact (pr2 (leftunitor_nat_z_iso V) (I_{V})). - apply identity_is_z_iso. 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.Isos. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Functors. Import BifunctorNotations. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Require Import UniMath.CategoryTheory.Monoidal.CategoriesOfMonoids. Import MonoidalNotations.