(x : A) (co_comult : x $-> tensor x x) (co_counit : x $-> unit) (co_coassoc : associator x x x $o fmap01 tensor x co_comult $o co_comult $== fmap10 tensor co_comult x $o co_comult) (co_left_counit : left_unitor x $o fmap10 tensor co_counit x $o co_comult $== Id x) (co_right_counit : right_unitor x $o fmap01 tensor x co_counit $o co_comult $== Id x) : IsComonoidObject x. Proof. snrapply Build_IsMonoidObject. - exact co_comult. - exact co_counit. - nrapply cate_moveR_eV. symmetry. nrefine (cat_assoc _ _ _ $@ _). rapply co_coassoc. - simpl; nrefine (_ $@ cat_idr _). nrapply cate_moveL_Ve. nrefine (cat_assoc_opp _ _ _ $@ _). exact co_left_counit. - simpl; nrefine (_ $@ cat_idr _). nrapply cate_moveL_Ve. nrefine (cat_assoc_opp _ _ _ $@ _). exact co_right_counit. Defined.
Require Import Basics.Overture Basics.Tactics. Require Import WildCat.Core WildCat.Equiv WildCat.Monoidal WildCat.Bifunctor Require Import abstract_algebra.