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