Lemma rassociator_lassociator_CAT {C D E F : category} (X : [C, D]) (Y : [D, E]) (Z : [E, F]) : rassociator_CAT X Y Z · lassociator_CAT _ _ _ = id2_CAT _. Proof. apply (nat_trans_eq F); intro c. apply id_right. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering.