Proposition local_property_in_cod_functor {C₁ C₂ : univ_cat_with_finlim} {F : functor_finlim C₁ C₂} {H₁ : P C₁} {H₂ : P C₂} (HF : cat_property_functor P H₁ H₂ F) : fiberwise_cat_property_functor (finlim_to_dfl_comp_cat_functor F) (local_property_in_cod _ H₁) (local_property_in_cod _ H₂). Proof. intro Γ. use (cat_property_functor_nat_z_iso_adj_equiv_f' P _ _ _ _ _ (local_property_fiber_functor P _ _ _ HF Γ)). - apply functor_identity. - apply functor_identity. - apply identity_functor_is_adj_equivalence. - apply identity_functor_is_adj_equivalence. - exact (nat_z_iso_id (slice_univ_cat_fiber F Γ)). 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.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.Limits.Terminal. 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.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.DispAdjunctions. Require Import UniMath.Bicategories.DisplayedBicats.DispBiequivalence. Require Import UniMath.Bicategories.DisplayedBicats.DispBuilders. Require Import UniMath.Bicategories.DisplayedBicats.DispPseudofunctor. Require Import UniMath.Bicategories.DisplayedBicats.DispTransformation. Require Import UniMath.Bicategories.DisplayedBicats.DispModification. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Require Import UniMath.Bicategories.PseudoFunctors.Examples.Identity. Require Import UniMath.Bicategories.PseudoFunctors.Examples.Composition. Require Import UniMath.Bicategories.Transformations.PseudoTransformation. Require Import UniMath.Bicategories.PseudoFunctors.Biequivalence. Require Import UniMath.Bicategories.ComprehensionCat.BicatOfCompCat. Require Import UniMath.Bicategories.ComprehensionCat.CompCatNotations. Require Import UniMath.Bicategories.ComprehensionCat.DFLCompCat. Require Import UniMath.Bicategories.ComprehensionCat.ComprehensionEso. Require Import UniMath.Bicategories.ComprehensionCat.Biequivalence.FinLimToDFLCompCat. Require Import UniMath.Bicategories.ComprehensionCat.Biequivalence.DFLCompCatToFinLim. Require Import UniMath.Bicategories.ComprehensionCat.Biequivalence.Unit. Require Import UniMath.Bicategories.ComprehensionCat.Biequivalence.Counit. Require Import UniMath.Bicategories.ComprehensionCat.Biequivalence.Biequiv. Require Import UniMath.Bicategories.ComprehensionCat.LocalProperty.LocalProperties. Require Import UniMath.Bicategories.ComprehensionCat.LocalProperty.DFLCompCatWithProp. Require Import UniMath.Bicategories.ComprehensionCat.LocalProperty.CatWithProp.