proposition: Lemma functorial_composition_pre_post (C D E: category) (F F' : [C, D]) (G G' : [D, E]) (f: [C, D]⟦F, F'⟧) (g: [D, E]⟦G, G'⟧) : # (functorial_composition _ _ _) (f,, g:precategory_binproduct [C, D] [D, E] ⟦(F,,G), (F',,G')⟧) = # (pre_comp_functor F) g · # (post_comp_functor G') f.
proof: Proof. apply (nat_trans_eq E). intro c. cbn. apply nat_trans_ax. Qed.
imports: UniMath.Foundations.PartD UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.UnitorsAndAssociatorsForEndofunctors