Definition disp_prebicat_ops_on_cat_to_univ_cat : disp_prebicat_ops disp_prebicat_1_id_comp_cells_on_cat_to_univ_cat. Proof. repeat split. - intros C₁ C₂ F CC₁ CC₂ FF. exact (@disp_id2 _ D _ _ _ _ _ FF). - intros C₁ C₂ F CC₁ CC₂ FF. exact (@disp_lunitor _ D _ _ _ _ _ FF). - intros C₁ C₂ F CC₁ CC₂ FF. exact (@disp_runitor _ D _ _ _ _ _ FF). - intros C₁ C₂ F CC₁ CC₂ FF. exact (@disp_linvunitor _ D _ _ _ _ _ FF). - intros C₁ C₂ F CC₁ CC₂ FF. exact (@disp_rinvunitor _ D _ _ _ _ _ FF). - intros C₁ C₂ C₃ C₄ F G H CC₁ CC₂ CC₃ CC₄ FF GG HH. exact (@disp_rassociator _ D _ _ _ _ _ _ _ _ _ _ _ FF GG HH). - intros C₁ C₂ C₃ C₄ F G H CC₁ CC₂ CC₃ CC₄ FF GG HH. exact (@disp_lassociator _ D _ _ _ _ _ _ _ _ _ _ _ FF GG HH). - intros C₁ C₂ F G H τ θ CC₁ CC₂ FF GG HH ττ θθ. exact (@disp_vcomp2 _ D _ _ _ _ _ _ _ _ _ _ _ _ ττ θθ). - intros C₁ C₂ C₃ F G₁ G₂ τ CC₁ CC₂ CC₃ FF GG₁ GG₂ ττ. exact (@disp_lwhisker _ D _ _ _ _ _ _ _ _ _ _ FF _ _ ττ). - intros C₁ C₂ C₃ F₁ F₂ G τ CC₁ CC₂ CC₃ FF₁ FF₂ GG ττ. exact (@disp_rwhisker _ D _ _ _ _ _ _ _ _ _ _ _ _ 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.