Definition disp_bicat_of_univ_cat_with_cat_property (P : cat_property) : disp_bicat bicat_of_univ_cat_with_finlim. Proof. use disp_subbicat. - exact (λ (C : univ_cat_with_finlim), P C). - exact (λ (C₁ C₂ : univ_cat_with_finlim) (H₁ : P C₁) (H₂ : P C₂) (F : functor_finlim C₁ C₂), cat_property_functor P H₁ H₂ F). - intros C H. apply cat_property_id_functor. - intros C₁ C₂ C₃ P₁ P₂ P₃ F G HF HG. exact (cat_property_comp_functor P HF HG). Defined.
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.DisplayedCats.Core. 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.DispUnivalence. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Sub1Cell. Require Import UniMath.Bicategories.ComprehensionCat.LocalProperty.LocalProperties.