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