Definition dfl_comp_cat_to_finlim_disp_psfunctor_local_property : disp_psfunctor (disp_bicat_of_cat_property_dfl_full_comp_cat P) (disp_bicat_of_univ_cat_with_cat_property P) dfl_comp_cat_to_finlim_psfunctor. Proof. use make_disp_psfunctor_contr. - apply disp_2cells_iscontr_disp_bicat_of_univ_cat_with_cat_property. - exact (λ C H, local_property_in_dfl_comp_cat C (pr1 H) ,, tt). - refine (λ _ _ _ _ _ HF, tt ,, local_property_in_dfl_comp_cat_functor _). exact (pr2 HF). 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.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.