Definition lift_functor_along_comp (G1 : functor C1 C2) (G2 : functor C2 C3) : nat_z_iso (lift_functor_along D3 F1 F1_eso F1_ff ((G1 ∙ G2) ∙ F3)) (lift_functor_along D2 F1 F1_eso F1_ff (G1 ∙ F2) ∙ lift_functor_along D3 F2 F2_eso F2_ff (G2 ∙ F3)). Proof. use (lift_nat_z_iso_along D3 F1 F1_eso F1_ff). set (l := lift_functor_along_comm D3 F2 F2_eso F2_ff (G2 ∙ F3)). set (l2_i := pre_whisker_on_nat_z_iso G1 (pr1 l) (pr2 l)). set (u := lift_functor_along_comm D2 F1 F1_eso F1_ff (G1 ∙ F2)). set (u2_i := post_whisker_z_iso_is_z_iso (pr1 u) (lift_functor_along D3 F2 F2_eso F2_ff ((G2 ∙ F3))) (pr2 u) ). transparent assert ( l2 : (nat_z_iso (functor_composite G1 (F2 ∙ lift_functor_along D3 F2 F2_eso F2_ff (G2 ∙ F3))) (functor_composite G1 (G2 ∙ F3)))). { use make_nat_z_iso. 2: exact l2_i. } transparent assert (u2 : (nat_z_iso (functor_composite (F1 ∙ lift_functor_along D2 F1 F1_eso F1_ff (G1 ∙ F2)) (lift_functor_along D3 F2 F2_eso F2_ff (G2 ∙ F3))) (functor_composite (G1 ∙ F2) (lift_functor_along D3 F2 F2_eso F2_ff (G2 ∙ F3))))). { use make_nat_z_iso. 2: exact u2_i. } use nat_z_iso_comp. 2: { apply lift_functor_along_comm. } use nat_z_iso_comp. 2: { exact (nat_z_iso_inv l2). } exact (nat_z_iso_inv u2). 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.