Definition make_is_local_property {P : cat_property} (H : ∏ (C : univ_cat_with_finlim) (x : C), P C → P (slice_univ_cat_with_finlim x)) (Hpb : ∏ (C : univ_cat_with_finlim) (p : P C) (x y : C) (f : x --> y), cat_property_functor P (H C y p) (H C x p) (slice_univ_cat_pb_finlim f)) (Hfib : ∏ (C₁ C₂ : univ_cat_with_finlim) (p₁ : P C₁) (p₂ : P C₂) (F : functor_finlim C₁ C₂) (HF : cat_property_functor P p₁ p₂ F) (x : C₁), cat_property_functor P (H C₁ x p₁) (H C₂ (F x) p₂) (slice_univ_cat_fiber F x)) : is_local_property P := H ,, Hpb ,, Hfib.
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.