Definition lift_functor_along_pair (H1 : functor C1 C1') (H2 : functor C2 C2') : nat_z_iso (lift_functor_along DD' FF FF_eso FF_ff (pair_functor H1 H2 ∙ pair_functor F1' F2')) (pair_functor (lift_functor_along D1' F1 F1_eso F1_ff (H1 ∙ F1')) (lift_functor_along D2' F2 F2_eso F2_ff (H2 ∙ F2'))). Proof. use (lift_nat_z_iso_along DD' FF FF_eso FF_ff). set (l := lift_functor_along_comm DD' FF FF_eso FF_ff (pair_functor H1 H2 ∙ pair_functor F1' F2')). use nat_z_iso_comp. 2: { exact l. } use nat_z_iso_comp. 3: { apply nat_z_iso_pair. } use nat_z_iso_comp. 2: { apply (nat_z_iso_inv (nat_z_iso_pair _ _ _ _)). } use nat_z_iso_between_pair ; apply (nat_z_iso_inv (lift_functor_along_comm _ _ _ _ _)). 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.