Definition post_whisker_fst_param {B C D P: category} {G H : B ⟶ C} (γ : G ⟹ H) (K : (P × C) ⟶ D): (functor_composite (pair_functor (functor_identity _) G) K) ⟹ (functor_composite (pair_functor (functor_identity _) H) K) := make_nat_trans _ _ _ (is_nat_trans_post_whisker_fst_param γ K).
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.