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 _)).
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.