{A : Type} `{Is1Cat A, !HasBinaryProducts A} {w x y z : A} (f : x $-> y) (g : w $-> x) (h : w $-> z) : fmap10 (fun x y => cat_binprod x y) f z $o cat_binprod_corec g h $== cat_binprod_corec (f $o g) h. Proof. snrapply cat_binprod_eta_pr. - refine (cat_assoc_opp _ _ _ $@ _). refine ((_ $@R _) $@ cat_assoc _ _ _ $@ (_ $@L _) $@ _^$). 1-3: nrapply cat_binprod_beta_pr1. - refine (cat_assoc_opp _ _ _ $@ _). refine ((_ $@R _) $@ cat_assoc _ _ _ $@ cat_idl _ $@ _ $@ _^$). 1-3: 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