fact: 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⟧.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.FunctorCategory