Definition disp_adjoint_equivalence {a b : C} (f : adjoint_equivalence a b) (aa : D a) (bb : D b) : UU := ∑ ff : aa -->[f] bb, disp_left_adjoint_equivalence f ff. Coercion disp_adjunction_of_adjoint_equivalence {a b : C} {f : adjoint_equivalence a b} {aa : D a} {bb : D b} (ff : disp_adjoint_equivalence f aa bb) : disp_adjunction f aa bb. Proof. refine (pr1 ff,, _). apply (disp_left_adjoint_of_left_adjoint_equivalence (pr2 ff)). Defined.
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.