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. apply (nat_trans_eq E). intro c. cbn. apply nat_trans_ax. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.UnitorsAndAssociatorsForEndofunctors.