{A : Type} `{HasEquivs A} {hbc : HasBinaryCoproducts A} (x y z : A) : cat_bincoprod x (cat_bincoprod y z) $<~> cat_bincoprod (cat_bincoprod x y) z. Proof. exact (@associator_cat_binprod A^op _ _ _ _ _ hbc x y z)^-1$. Defined.
Require Import Basics.Overture Basics.Tactics Basics.Decidable. Require Import Types.Bool. Require Import WildCat.Core WildCat.Equiv WildCat.Forall WildCat.NatTrans