fact: Definition associator_funclass (α' : associator): ∏ x : ob ((C ⊠ C) ⊠ C), assoc_left x --> assoc_right x := pr1 (nat_z_iso_to_trans α').
imports: UniMath.Foundations.PartD UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.ProductCategory UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.whiskering