Definition pre_whisker_in_funcat (A B C : category) (F : [A, B]) {G H : [B, C]} (γ : [B, C]⟦G, H⟧) : [A, C]⟦functor_compose F G, functor_compose F H⟧. Proof. exact (pre_whisker (F: A ⟶ B) γ). 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.