Strict monoidal categories lack coherence laws

[anuyts]

In Cubical.Categories.Monoidal.Base, there is a type MonoidalStr of non-strict monoidal structures and a type StrictMonStr of strict ones. One would expect the following results:

• Strict structures give rise to non-strict ones
• For univalent categories, this is an isomorphism.

However, I think the first result doesn't even hold (unless your object type is a set) as the strict structure lacks coherence laws.