{a b c : A} (f : a $-> b) (g : a $-> c) : cat_binprod_swap b c $o cat_binprod_corec f g $== cat_binprod_corec g f. Proof. nrapply cat_binprod_eta_pr. - refine (cat_assoc_opp _ _ _ $@ (_ $@R _) $@ (_ $@ _^$)). 1,3: nrapply cat_binprod_beta_pr1. nrapply cat_binprod_beta_pr2. - refine (cat_assoc_opp _ _ _ $@ (_ $@R _) $@ (_ $@ _^$)). 1,3: nrapply cat_binprod_beta_pr2. nrapply cat_binprod_beta_pr1. 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