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