{a a' b b' c c' : A} (f : a $-> a') (g : b $-> b') (h : c $-> c') : cat_binprod_twist a' b' c' $o fmap11 (fun x y => cat_binprod x y) f (fmap11 (fun x y => cat_binprod x y) g h) $== fmap11 (fun x y => cat_binprod x y) g (fmap11 (fun x y => cat_binprod x y) f h) $o cat_binprod_twist a b c. Proof. nrapply cat_binprod_eta_pr. - refine (cat_assoc_opp _ _ _ $@ _). nrefine ((cat_binprod_beta_pr1 _ _ $@R _) $@ _). nrefine (cat_assoc _ _ _ $@ _). nrefine ((_ $@L _) $@ _). 1: nrapply cat_pr2_fmap11_binprod. nrefine (cat_assoc_opp _ _ _ $@ _). nrefine ((_ $@R _) $@ _). 1: nrapply cat_pr1_fmap11_binprod. nrefine (_ $@ cat_assoc _ _ _). refine (_ $@ (_^$ $@R _)). 2: nrapply cat_pr1_fmap11_binprod. refine (cat_assoc _ _ _ $@ (_ $@L _^$) $@ (cat_assoc _ _ _)^$). nrapply cat_binprod_beta_pr1. - nrefine (cat_assoc_opp _ _ _ $@ (cat_binprod_beta_pr2 _ _ $@R _) $@ _). nrefine (_ $@ cat_assoc _ _ _). refine (_ $@ (_^$ $@R _)). 2: nrapply cat_pr2_fmap11_binprod. refine (_ $@ (_ $@L _^$) $@ (cat_assoc _ _ _)^$). 2: nrapply cat_binprod_beta_pr2. refine (_^$ $@ _ $@ _). 1,3: rapply fmap11_comp. rapply fmap22. 1: exact (cat_idl _ $@ (cat_idr _)^$). nrapply cat_binprod_beta_pr2. 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