Proposition cat_property_functor_nat_z_iso_adj_equiv_f' {C₁ C₂ D₁ D₂ : univ_cat_with_finlim} {HC₁ : P C₁} {HC₂ : P C₂} {HD₁ : P D₁} {HD₂ : P D₂} {EC : functor C₁ C₂} {ED : functor D₁ D₂} (HEC : adj_equivalence_of_cats EC) (HED : adj_equivalence_of_cats ED) (F : functor_finlim C₁ D₁) (G : functor_finlim C₂ D₂) (τ : nat_z_iso (pr1 F ∙ ED) (EC ∙ pr1 G)) (HF : cat_property_functor P HC₁ HD₁ F) : cat_property_functor P HC₂ HD₂ G. Proof. exact (cat_property_functor_nat_z_iso_adj_equiv_f (EC := make_functor_finlim_adjequiv _ HEC) (ED := make_functor_finlim_adjequiv _ HED) HEC HED F G τ HF). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Preservation. Require Import UniMath.CategoryTheory.Limits.PreservationProperties. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Equivalences.CompositesAndInverses. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.FiberCod. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.CodFunctor. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.CodLimits. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.Core.Examples.StructuredCategories. Require Import UniMath.Bicategories.ComprehensionCat.BicatOfCompCat. Require Import UniMath.Bicategories.ComprehensionCat.DFLCompCat.