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_finlim C₁ C₂} {ED : functor_finlim D₁ D₂} (HEC : adj_equivalence_of_cats (pr1 EC)) (HED : adj_equivalence_of_cats (pr1 ED)) (F : functor_finlim C₁ D₁) (G : functor_finlim C₂ D₂) (τ : nat_z_iso (pr1 F ∙ pr1 ED) (pr1 EC ∙ pr1 G)) (HF : cat_property_functor P HC₁ HD₁ F) : cat_property_functor P HC₂ HD₂ G. Proof. refine (cat_property_functor_nat_z_iso_adj_equiv_f_help (EC ,, _) (ED ,, _) _ _ τ HF). - use left_adjoint_equivalence_univ_cat_with_finlim. exact HEC. - use left_adjoint_equivalence_univ_cat_with_finlim. exact HED. 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.