proposition: 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: Proof. apply (nat_trans_eq E); intro c. cbn. do 3 rewrite id_left. apply functor_id. Qed.
imports: UniMath.Foundations.PartD UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering