{x : A} `{!IsComonoidObject x} : right_unitor x $o fmap01 tensor x co_counit $o co_comult $== Id x. Proof. refine (cat_assoc _ _ _ $@ _). apply cate_moveR_Me. refine (_ $@ (cat_idr _)^$). exact (mo_right_unit (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.