fact: Definition nat_trans_data_post_whisker_fst_param {B C D P: category} {G H : B ⟶ C} (γ : G ⟹ H) (K : (P × C) ⟶ D): nat_trans_data (functor_composite (pair_functor (functor_identity _) G) K) (functor_composite (pair_functor (functor_identity _) H) K) := λ pb : P × B, #K ((identity (ob1 pb),, γ (ob2 pb)): (P × C)⟦ob1 pb,, G(ob2 pb), ob1 pb,, H(ob2 pb)⟧).
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.opp_precat