proposition: Lemma to_assoc {x y : PA} (f g h : PA⟦x, y⟧) : to_binop _ _ (to_binop _ _ f g) h = to_binop _ _ f (to_binop _ _ g h).
proof: Proof. apply (assocax (to_abgr x y)). Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.CategoriesWithBinOps UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Core.Functors