fact: Definition vassocr {a b : C} {f g h k : C⟦a, b⟧} (x : f ==> g) (y : g ==> h) (z : h ==> k) : x • (y • z) = (x • y) • z := pr1 (pr2 (pr2 (pr2 C))) _ _ _ _ _ _ x y z.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Univalence