(x : A) `{!IsComonoidObject x} (cco_cocomm : braid x x $o co_comult $== co_comult) : IsCocommutativeComonoidObject x. Proof. snrapply Build_IsCommutativeMonoidObject. - exact _. - exact cco_cocomm. Defined.
Require Import Basics.Overture Basics.Tactics. Require Import WildCat.Core WildCat.Equiv WildCat.Monoidal WildCat.Bifunctor Require Import abstract_algebra.