{A} (tensor : A -> A -> A) (unit : A) `{IsMonoidal A tensor unit} : (left_unitor unit : tensor unit unit $-> _) $== right_unitor unit. Proof. refine ((cate_moveR_eV _ _ _ (isnat_natequiv left_unitor (left_unitor unit)))^$ $@ _). apply cate_moveR_eV. refine (_ $@ (_ $@L left_unitor_associator _ _ _ _)^$). nrefine (_ $@ (_ $@R _) $@ cat_assoc _ _ _). 2: rapply (isnat_natequiv right_unitor _)^$. nrefine ((_ $@L _) $@ cat_assoc_opp _ _ _). refine (triangle_identity _ _ _ _ _ _ $@ _). nrefine (_ $@R _). nrapply cate_monic_equiv. exact (isnat_natequiv right_unitor (right_unitor unit)). 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.