proposition: 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: Proof. exists (pre_whisker F α). exact (pre_whisker_on_nat_z_iso F α (pr2 α)). Defined.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.FunctorCategory