Definition disp_prebicat_1_id_comp_cells_on_cat_to_univ_cat : disp_prebicat_1_id_comp_cells bicat_of_univ_cats. Proof. simple refine (_ ,, _). - exact disp_cat_data_on_cat_to_univ_cat. - exact (λ (C₁ C₂ : univalent_category) (F G : bicat_of_cats ⟦ pr1 C₁ , pr1 C₂ ⟧) (τ : F ==> G) (CC₁ : D (pr1 C₁)) (CC₂ : D (pr1 C₂)) (FF : CC₁ -->[ F ] CC₂) (GG : CC₁ -->[ G ] CC₂), FF ==>[ τ ] GG). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Examples.BicatOfCats. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Require Import UniMath.Bicategories.PseudoFunctors.Examples.BicatOfCatToUnivCat. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence. Require Import UniMath.Bicategories.DisplayedBicats.DispPseudofunctor.