Definition is_right_adjoint_to_right_adjoint {C₁ C₂ : bicat_of_univ_cats} {R : C₁ --> C₂} (HR : is_right_adjoint R) : internal_right_adj R. Proof. simple refine ((pr1 HR ,, (pr112 HR ,, pr212 HR)) ,, _). split. - abstract (use nat_trans_eq ; [ apply homset_property | ] ; intro x ; cbn ; rewrite !id_left, !id_right ; apply (pr122 HR)). - abstract (use nat_trans_eq ; [ apply homset_property | ] ; intro x ; cbn ; rewrite !id_left, !id_right ; apply (pr222 HR)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.catiso. Require Import UniMath.CategoryTheory.CategoryEquality. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.Core.Univalence.