Lemma vassoc4 {a b : C} {f g h i j: C ⟦a, b⟧} (w : f ==> g) (x : g ==> h) (y : h ==> i) (z : i ==> j) : w • (x • (y • z)) = w • (x • y) • z. Proof. repeat rewrite vassocr. apply idpath. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.PrecategoryBinProduct.