{A : Type} `{HasEquivs A} `{!HasBinaryCoproducts A} : Associator (fun x y => cat_bincoprod x y). Proof. unfold Associator. snrapply associator_op'. 1: exact _. nrapply associator_cat_binprod. Defined.
Require Import Basics.Overture Basics.Tactics Basics.Decidable. Require Import Types.Bool. Require Import WildCat.Core WildCat.Equiv WildCat.Forall WildCat.NatTrans