Definition pre_whisker {A B C : precategory_data} (F : functor_data A B) {G H : functor_data B C} (gamma : nat_trans G H) : nat_trans (functor_composite_data F G) (functor_composite_data F H). Proof. exists (λ a, pr1 gamma (pr1 F a)). apply is_nat_trans_pre_whisker. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.FunctorCategory.