Definition disp_adjunction_data {C C' : category} (A : adjunction_data C C') (F := left_functor A) (G := right_functor A) (eta := adjunit A) (eps := adjcounit A) (D : disp_cat C) (D' : disp_cat C') : UU := ∑ (FF : disp_functor F D D') (GG : disp_functor G D' D), (disp_nat_trans eta (disp_functor_identity _ ) (disp_functor_composite FF GG)) × (disp_nat_trans eps (disp_functor_composite GG FF) (disp_functor_identity _ )).
Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.NaturalTransformations. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber.