proposition: Lemma nat_z_iso_between_pair {C1 C2 D1 D2 : category} {F1 F1' : functor C1 D1} {G1 G1' : functor C2 D2} (α : nat_z_iso F1 F1') (β : nat_z_iso G1 G1') : nat_z_iso (pair_functor F1 G1) (pair_functor F1' G1').
proof: Proof. use make_nat_z_iso. - use make_nat_trans. + intro ; apply catbinprodmor ; [apply α | apply β]. + abstract (intro ; intros ; use total2_paths_f ; [apply (pr1 α) | rewrite transportf_const ; apply (pr1 β)]). - intro. use tpair. + apply catbinprodmor ; [apply (pr2 α) | apply (pr2 β)]. + abstract (split ; (use total2_paths_f ; [apply (pr2 α) | rewrite transportf_const ; apply (pr2 β)])). Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.Equivalences.FullyFaithful UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.precomp_ess_surj UniMath.CategoryTheory.precomp_fully_faithful UniMath.CategoryTheory.PrecategoryBinProduct