Lemma post_whisker_nat_z_iso {C D E : category} {G1 G2 : functor C D} (α : nat_z_iso G1 G2) (F : functor D E) : nat_z_iso (functor_composite G1 F) (functor_composite G2 F). Proof. exists (post_whisker α F). exact (post_whisker_z_iso_is_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.