Definition map1cells_disp_left_adjoint_equivalence (HD : is_univalent_2 D) {F₀ G₀ : ps_base C D} {η₀ : F₀ --> G₀} (Hη₀ : left_adjoint_equivalence η₀) (F₁ : map1cells_disp_bicat F₀) (G₁ : map1cells_disp_bicat G₀) (η₁ : F₁ -->[ η₀ ] G₁) : disp_left_adjoint_equivalence Hη₀ η₁ := map1cells_disp_left_adjoint_equivalence_help HD (η₀ ,, Hη₀) F₁ G₁ η₁.
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.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.DisplayedBicats.DispAdjunctions. Require Import UniMath.Bicategories.DisplayedBicats.DispInvertibles. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence.