(f : cat_bincoprod x y $-> z) : cat_bincoprod_rec (f $o cat_inl) (f $o cat_inr) $== f := @cat_binprod_eta A^op _ _ _ _ x y _ _ f.
Require Import Basics.Overture Basics.Tactics Basics.Decidable. Require Import Types.Bool. Require Import WildCat.Core WildCat.Equiv WildCat.Forall WildCat.NatTrans