Lemma lassociator_lassociator_CAT {A B C D E : category} (F : [A, B]) (G : [B, C]) (H : [C, D]) (I : [D, E]) : lwhisker_CAT F (lassociator_CAT G H I) · lassociator_CAT _ (functor_compose G H) _ · (rwhisker_CAT I (lassociator_CAT _ _ _)) = lassociator_CAT F G (functor_compose H I) · lassociator_CAT (functor_compose F G) _ _. Proof. apply (nat_trans_eq E); intro c. cbn. do 3 rewrite id_left. apply functor_id. 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.