fact: 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 _ )).
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.PartA UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.NaturalTransformations UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Fiber