Definition disp_left_adjoint_data {a b : C} {f : a --> b} (αd : left_adjoint_data f) {aa : D a} {bb : D b} (ff : aa -->[f] bb) : UU := ∑ (gg : bb -->[left_adjoint_right_adjoint αd] aa), (id_disp aa ==>[left_adjoint_unit αd] ff ;; gg) × (gg ;; ff ==>[left_adjoint_counit αd] id_disp bb).
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.DisplayedBicats.DispInvertibles. Require Import UniMath.Bicategories.Core.Univalence.