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. now rewrite functor_comp. Qed.
Require Import UniMath.Foundations.Propositions. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Univalence. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.TransportMorphisms. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence.