Definition equiv_cat_to_adj_equiv {C D : bicat_of_univ_cats} (F : C --> D) : adj_equivalence_of_cats F → left_adjoint_equivalence F. Proof. intros A. use tpair. - use tpair. + apply A. + split ; cbn. * exact (pr1 (pr121 A)). * exact (pr2 (pr121 A)). - split ; split. + abstract (apply nat_trans_eq ; [ apply homset_property | ] ; intro x ; cbn ; rewrite id_left, !id_right ; apply (pr2(pr2(pr1 A)))). + abstract (apply nat_trans_eq ; [ apply homset_property | ] ; intro x ; cbn ; rewrite id_left, !id_right ; apply (pr2(pr2(pr1 A)))). + apply is_nat_z_iso_to_is_invertible_2cell. intro x. apply (pr2 A). + apply is_nat_z_iso_to_is_invertible_2cell. intro x. apply (pr2 A). 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.