{A : Type} `{HasEquivs A} (F : A -> A -> A) `{!Is0Bifunctor F, !Is1Bifunctor F} (associator : forall a b c, F a (F b c) $<~> F (F a b) c) (isnat_assoc : Is1Natural (fun '(a, b, c) => F a (F b c)) (fun '(a, b, c) => F (F a b) c) (fun '(a, b, c) => associator a b c)) : Associator F. Proof. snrapply Build_NatEquiv. - intros [[a b] c]. exact (associator a b c). - exact isnat_assoc. Defined.
Require Import Basics.Overture Basics.Tactics Types.Forall. Require Import WildCat.Core WildCat.Bifunctor WildCat.Prod WildCat.Equiv. Require Import WildCat.NatTrans WildCat.Opposite.