Definition lift_nat_z_iso_along {G₁ G₂ : C₂ ⟶ D} (α : nat_z_iso (F ∙ G₁) (F ∙ G₂)) : nat_z_iso G₁ G₂. Proof. exists (lift_nat_trans_along α). use is_functor_z_iso_pointwise_if_z_iso. { apply homset_property. } set (β := (z_iso_from_nat_z_iso (homset_property _) α)). set (ff_precomp := (fully_faithful_from_equivalence [C₂, pr1 D] [C₁, pr1 D] (pre_composition_functor C₁ C₂ (pr1 D) F) precomp_adjoint_equivalence)). exact (fully_faithful_reflects_iso_proof [C₂, pr1 D] [C₁, pr1 D] (pre_composition_functor _ _ D F) ff_precomp _ _ β ). 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.