{A} (tensor : A -> A -> A) (unit : A) `{IsMonoidal A tensor unit} (x y : A) : (left_unitor (tensor x y) : _ $-> _) $== fmap10 tensor (left_unitor x) y $o associator unit x y. Proof. refine ((cate_moveR_eV _ _ _ (isnat_natequiv left_unitor _))^$ $@ ((_ $@L _) $@R _) $@ cate_moveR_eV _ _ _ (isnat_natequiv left_unitor _)). refine (_ $@ (fmap01_comp _ _ _ _)^$). refine (_ $@ (cate_moveR_Ve _ _ _ (associator_nat_m _ _ _)^$ $@R _)). nrefine (_ $@ cat_assoc_opp _ _ _). change (fmap (tensor ?x) ?f) with (fmap01 tensor x f). change (cate_fun' _ _ (cat_tensor_left_unitor ?x)) with (cate_fun (cat_tensor_left_unitor x)). apply cate_moveL_Ve. refine ((_ $@L triangle_identity _ _ _ _ _ _) $@ _). nrefine (cat_assoc_opp _ _ _ $@ _ $@ cat_assoc_opp _ _ _). refine (_ $@ ((fmap20 _ (triangle_identity _ _ _ _ _ _) _ $@ fmap10_comp _ _ _ _)^$ $@R _)). refine (_ $@ cat_assoc_opp _ _ _). refine (_ $@ (_ $@L (pentagon_identity _ _ _ _ _ _ $@ cat_assoc _ _ _))). refine ((_ $@R _) $@ cat_assoc _ _ _). exact (associator_nat_l _ _ _). 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.