{x : A} `{!IsCocommutativeComonoidObject x} : braid x x $o co_comult $== co_comult. Proof. exact (cmo_comm (A:=A^op) (tensor:=tensor) (unit:=unit) (x:=x)). Defined.
Require Import Basics.Overture Basics.Tactics. Require Import WildCat.Core WildCat.Equiv WildCat.Monoidal WildCat.Bifunctor Require Import abstract_algebra.