Definition is_catiso_left_adjoint_equivalence {C D : univalent_category} (F : C ⟶ D) : is_catiso F ≃ @left_adjoint_equivalence bicat_of_univ_cats C D F. Proof. use weqimplimpl. - exact (is_catiso_to_left_adjoint_equivalence F). - exact (left_adjoint_equivalence_to_is_catiso F). - apply isaprop_is_catiso. - apply invproofirrelevance. intros A₁ A₂. apply unique_internal_adjoint_equivalence. apply univalent_cat_is_univalent_2_1. 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.