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