{A : Type} `{HasEquivs A} {F : A -> A -> A} `{!Is0Bifunctor F, !Is1Bifunctor F, !Associator F} : forall a b c, F a (F b c) $<~> F (F a b) c := fun a b c => associator_uncurried (a, b, c).
Require Import Basics.Overture Basics.Tactics Types.Forall. Require Import WildCat.Core WildCat.Bifunctor WildCat.Prod WildCat.Equiv. Require Import WildCat.NatTrans WildCat.Opposite.