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. 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Equivalences.FullyFaithful. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.precomp_ess_surj. Require Import UniMath.CategoryTheory.precomp_fully_faithful. Require Import UniMath.CategoryTheory.PrecategoryBinProduct.