Lemma pre_whisker_nat_z_iso {C D E : category} (F : functor C D) {G1 G2 : functor D E} (α : nat_z_iso G1 G2) : nat_z_iso (functor_composite F G1) (functor_composite F G2). Proof. exists (pre_whisker F α). exact (pre_whisker_on_nat_z_iso F α (pr2 α)). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.FunctorCategory.