proposition: Lemma lunitor_lwhisker_CAT {A B C : category} (F : [A, B]) (G : [B, C]) : rassociator_CAT F (id1_CAT B) G · (lwhisker_CAT F (lunitor_CAT G)) = rwhisker_CAT G (runitor_CAT F).
proof: Proof. apply (nat_trans_eq C); intro c. cbn. rewrite id_left. apply pathsinv0, 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