{w x y z} (f : w $-> x) (g : w $-> y) (h : w $-> z) : associator_cat_binprod x y z $o cat_binprod_corec f (cat_binprod_corec g h) $== cat_binprod_corec (cat_binprod_corec f g) h. Proof. nrefine ((associator_twist'_unfold _ _ _ _ _ _ _ _ $@R _) $@ _). nrefine ((cat_assoc_opp _ _ _ $@R _) $@ cat_assoc _ _ _ $@ (_ $@L (_ $@ _)) $@ _). 1: nrapply cat_binprod_fmap01_corec. 1: rapply (cat_binprod_corec_eta _ _ _ _ (Id _)). 1: nrapply cat_binprod_swap_corec. nrefine (cat_assoc _ _ _ $@ (_ $@L _) $@ _). 1: nrapply cat_binprod_twist_corec. nrapply cat_binprod_swap_corec. Defined.
Require Import Basics.Equivalences Basics.Overture Basics.Tactics. Require Import Types.Bool Types.Prod Types.Forall. Require Import WildCat.Bifunctor WildCat.Core WildCat.Equiv WildCat.EquivGpd