{A : Type} {tensor : A -> A -> A} {unit : A} `{HasEquivs A, !Is0Bifunctor tensor, !Is1Bifunctor tensor} `{!Associator tensor, !LeftUnitor tensor unit, !RightUnitor tensor unit, !Braiding tensor} {x : A} `{C : !IsCocommutativeComonoidObject (A:=A^op) tensor unit x} : IsCommutativeMonoidObject tensor unit x. Proof. snrapply Build_IsCommutativeMonoidObject. - nrapply mo_co_op. rapply co_cco. - exact (cco_cocomm (A:=A^op) tensor unit). Defined.
Require Import Basics.Overture Basics.Tactics. Require Import WildCat.Core WildCat.Equiv WildCat.Monoidal WildCat.Bifunctor Require Import abstract_algebra.