Lemma is_nat_trans_post_whisker_snd_param {B C D P: category} {G H : B ⟶ C} (γ : G ⟹ H) (K : (C × P) ⟶ D): is_nat_trans _ _ (nat_trans_data_post_whisker_snd_param γ K). Proof. intros bp bp' f. cbn. unfold nat_trans_data_post_whisker_snd_param. eapply pathscomp0. 2: { apply functor_comp. } eapply pathscomp0. { apply pathsinv0. apply functor_comp. } apply maponpaths. unfold compose; cbn. rewrite id_left. rewrite id_right. apply (maponpaths (λ x, make_dirprod x (pr2 f))). apply (nat_trans_ax γ). Qed.
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.