Definition lift_disp_prebicat_ops : disp_prebicat_ops lift_disp_prebicat_1_id_comp_cells. Proof. repeat split. - intros. apply disp_id2. - intros. apply disp_lunitor. - intros. apply disp_runitor. - intros. apply disp_linvunitor. - intros. apply disp_rinvunitor. - intros. apply disp_rassociator. - intros. apply disp_lassociator. - intros x y f g h τ θ xx yy zz ff gg ττ θθ. exact (ττ •• θθ). - intros x y z f g₁ g₂ τ xx yy zz ff gg₁ gg₂ ττ. exact (ff ◃◃ ττ). - intros x y z f₁ f₂ g τ xx yy zz ff₁ ff₂ gg ττ. exact (ττ ▹▹ gg). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.DisplayedBicats.DispInvertibles. Require Import UniMath.Bicategories.DisplayedBicats.DispAdjunctions. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence. Section FromLift. End FromLift.