proposition: Lemma functor_comp_pw {C C' D D' : precategory} hsD hsD' (F : [C,D,hsD] ⟶ [C',D',hsD']) {a b c} (f : [C,D,hsD] ⟦ a, b ⟧) (g : [C,D,hsD] ⟦ b, c ⟧) (x :C') : (# F f:nat_trans _ _) x · (# F g:nat_trans _ _) x = ((# F (f · g)) : nat_trans _ _ ) x .
proof: Proof. now rewrite functor_comp. Qed.
imports: UniMath.Foundations.Propositions UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Univalence UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.TransportMorphisms UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence