fact: Definition right_adjoint_over_data {C C' : category} {A : adjunction_data C C'} {D : disp_cat C} {D' : disp_cat C'} (FF : disp_functor (left_functor A) D D') : UU := ∑ (GG : disp_functor (right_functor A) D' D), (disp_nat_trans (adjunit A) (disp_functor_identity _) (disp_functor_composite FF GG)) × (disp_nat_trans (adjcounit A ) (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