Definition compositor_disp_left_adjequiv {HD : is_univalent_2 D} {F G : map1cells C D} (η : adjoint_equivalence F G) {F₂ : compositor_disp_cat F} {G₂ : compositor_disp_cat G} (η₂ : F₂ -->[ η ] G₂) : disp_left_adjoint_equivalence η η₂. Proof. revert F G η F₂ G₂ η₂. use J_2_0. - apply map1cells_is_univalent_2_0. exact HD. - intros F F₂ G₂ η₂. apply compositor_disp_left_adjequiv_over_id. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.PseudoFunctors.Display.Base. Require Import UniMath.Bicategories.PseudoFunctors.Display.Map1Cells. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.DisplayedBicats.Examples.DisplayedCatToBicat. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence.