proposition: Lemma nat_z_iso_pair {C1 C2 D1 D2 E1 E2 : category} (F1 : functor C1 D1) (F2 : functor D1 E1) (G1 : functor C2 D2) (G2 : functor D2 E2) : nat_z_iso (pair_functor (F1 ∙ F2) (G1 ∙ G2)) (pair_functor F1 G1 ∙ pair_functor F2 G2).
proof: Proof. use make_nat_z_iso. - use make_nat_trans. + intro ; apply catbinprodmor ; apply identity. + abstract (intro ; intros ; use total2_paths_f ; [ exact (id_right _ @ ! id_left _) | rewrite transportf_const ; exact (id_right _ @ ! id_left _) ]). - intro. use make_is_z_isomorphism. + apply catbinprodmor ; apply identity. + abstract (split ; (use total2_paths_f ; [ apply id_right | rewrite transportf_const ; apply id_right ])). 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