Proposition cat_property_functor_nat_z_iso_adj_equiv_f_help {C₁ C₂ D₁ D₂ : univ_cat_with_finlim} {HC₁ : P C₁} {HC₂ : P C₂} {HD₁ : P D₁} {HD₂ : P D₂} (EC : adjoint_equivalence C₁ C₂) (ED : adjoint_equivalence D₁ D₂) (F : functor_finlim C₁ D₁) (G : functor_finlim C₂ D₂) (τ : nat_z_iso (pr1 F ∙ pr11 ED) (pr11 EC ∙ pr1 G)) (HF : cat_property_functor P HC₁ HD₁ F) : cat_property_functor P HC₂ HD₂ G. Proof. revert C₁ C₂ EC D₁ D₂ ED HC₁ HC₂ HD₁ HD₂ F G τ HF. use J_2_0. { exact is_univalent_2_0_bicat_of_univ_cat_with_finlim. } intros C. use J_2_0. { exact is_univalent_2_0_bicat_of_univ_cat_with_finlim. } intros D HC₁ HC₂ HD₁ HD₂ F G τ HF. assert (HC₁ = HC₂) as p. { apply isaprop_cat_property_ob. } induction p. assert (HD₁ = HD₂) as p. { apply isaprop_cat_property_ob. } induction p. use (cat_property_functor_nat_z_iso_f τ). cbn. refine (transportf _ _ HF). apply idpath. 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.