{w x y z : A} (f : w $-> x) (g : w $-> y) (h : w $-> z) : cat_binprod_twist x y z $o cat_binprod_corec f (cat_binprod_corec g h) $== cat_binprod_corec g (cat_binprod_corec f h). Proof. nrapply cat_binprod_eta_pr. - nrefine (cat_assoc_opp _ _ _ $@ _). refine ((_ $@R _) $@ cat_assoc _ _ _ $@ (_ $@L _) $@ (_ $@ _^$)). 1: nrapply cat_binprod_pr1_twist. 1: nrapply cat_binprod_beta_pr2. 1,2: nrapply cat_binprod_beta_pr1. - refine (cat_assoc_opp _ _ _ $@ (_ $@R _) $@ _ $@ (cat_binprod_beta_pr2 _ _)^$). 1: nrapply cat_binprod_beta_pr2. nrefine (cat_binprod_fmap01_corec _ _ _ $@ _). nrapply cat_binprod_corec_eta. 1: exact (Id _). 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