Definition disp_bicat_of_cat_property_dfl_full_comp_cat (P : cat_property) : disp_bicat bicat_of_dfl_full_comp_cat. Proof. use disp_subbicat. - exact (λ (C : dfl_full_comp_cat), fiberwise_cat_property P C). - exact (λ (C₁ C₂ : dfl_full_comp_cat) (H₁ : fiberwise_cat_property P C₁) (H₂ : fiberwise_cat_property P C₂) (F : dfl_full_comp_cat_functor C₁ C₂), fiberwise_cat_property_functor F H₁ H₂). - abstract (intros C H x ; exact (cat_property_fiber_functor_id' P C x (H x))). - abstract (intros C₁ C₂ C₃ H₁ H₂ H₃ F G HF HG x ; exact (cat_property_fiber_functor_comp P (HF x) (HG _))). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. 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.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence. Require Import UniMath.Bicategories.DisplayedBicats.Examples.LiftDispBicat. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Sub1Cell. Require Import UniMath.Bicategories.ComprehensionCat.BicatOfCompCat. Require Import UniMath.Bicategories.ComprehensionCat.DFLCompCat. Require Import UniMath.Bicategories.ComprehensionCat.LocalProperty.LocalProperties.