Definition right_adjoint_to_is_right_adjoint {C₁ C₂ : bicat_of_univ_cats} {R : C₁ --> C₂} (HR : internal_right_adj R) : is_right_adjoint R. Proof. simple refine (pr11 HR ,, ((pr121 HR ,, pr221 HR) ,, _)). split. - abstract (intro x ; cbn ; pose (nat_trans_eq_pointwise (pr12 HR) x) as p ; cbn in p ; rewrite !id_left, !id_right in p ; exact p). - abstract (intro x ; cbn ; pose (nat_trans_eq_pointwise (pr22 HR) x) as p ; cbn in p ; rewrite !id_left, !id_right in p ; exact p). 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.