{A} (tensor : A -> A -> A) (unit : A) `{IsMonoidal A tensor unit} (x y : A) : (fmap01 tensor x (right_unitor y) : _ $-> _) $== right_unitor (tensor x y) $o associator x y unit. Proof. refine ((cate_moveR_eV _ _ _ (isnat_natequiv right_unitor _))^$ $@ ((_ $@L _) $@R _) $@ cate_moveR_eV _ _ _ (isnat_natequiv right_unitor _)). refine (_ $@ (fmap10_comp tensor _ _ _)^$). refine ((cate_moveR_eV _ _ _ (associator_nat_m _ _ _))^$ $@ _). refine (_ $@ (cate_moveR_eV _ _ _ (triangle_identity _ _ _ _ _ _) $@R _)). apply cate_moveR_eV. refine ((_ $@L (fmap02 _ _ (cate_moveR_eV _ _ _ (triangle_identity _ _ _ _ _ _))^$ $@ fmap01_comp _ _ _ _)) $@ _). refine (cat_assoc_opp _ _ _ $@ _). nrefine ((associator_nat_r _ _ _ $@R _) $@ cat_assoc _ _ _ $@ _). do 2 nrefine (_ $@ cat_assoc_opp _ _ _). refine (_ $@L _). refine ((_ $@L (emap_inv' _ _)^$) $@ _). apply cate_moveR_eV. refine (_ $@ (_ $@L cate_buildequiv_fun _)^$). nrefine (_ $@ cat_assoc_opp _ _ _). apply cate_moveL_Ve. rapply pentagon_identity. Defined.
Require Import Basics.Overture Basics.Tactics Types.Forall. Require Import WildCat.Core WildCat.Bifunctor WildCat.Prod WildCat.Equiv. Require Import WildCat.NatTrans WildCat.Opposite.