Definition constantly_unit_functor_is_symmetric (S : symmetric V) : is_symmetric_monoidal_functor S S constantly_unit_functor_fmonoidal. Proof. use constant_functor_is_symmetric. cbn. refine (_ @ id_left _). apply maponpaths_2. apply (sym_mon_braiding_id (V,,S)). 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.