Definition right_adjoint_weq_is_right_adjoint {C₁ C₂ : bicat_of_univ_cats} (R : C₁ --> C₂) : internal_right_adj R ≃ is_right_adjoint R. Proof. use make_weq. - exact right_adjoint_to_is_right_adjoint. - use isweq_iso. + exact is_right_adjoint_to_right_adjoint. + abstract (intro HL ; use subtypePath ; [ intro ; apply isapropdirprod ; apply cellset_property | ] ; apply idpath). + abstract (intro HL ; refine (maponpaths (λ z, _ ,, z) _) ; use subtypePath ; [ | apply idpath ] ; intro ; apply isapropdirprod ; use impred ; intro ; apply homset_property). 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.