Definition monoidal_struct_equiv_monoidal (C : category) : monoidal_struct C ≃ monoidal C. Proof. use weq_iso. - exact monoidal_struct_to_monoidal. - exact monoidal_to_monoidal_struct. - apply idpath. - apply idpath. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories.