Definition adj_equiv_to_equiv_cat {C D : bicat_of_univ_cats} (F : C --> D) : left_adjoint_equivalence F → adj_equivalence_of_cats F. Proof. intros A. use make_adj_equivalence_of_cats. - exact (left_adjoint_right_adjoint A). - exact (left_adjoint_unit A). - exact (left_adjoint_counit A). - split. + abstract (intro x ; cbn ; pose (nat_trans_eq_pointwise (internal_triangle1 A) x) as p ; cbn in p ; rewrite !id_left, !id_right in p ; exact p). + abstract (intro x ; cbn ; pose (nat_trans_eq_pointwise (internal_triangle2 A) x) as p ; cbn in p ; rewrite !id_left, !id_right in p ; exact p). - split. + intro X. apply (invertible_2cell_to_nat_z_iso _ _ (left_equivalence_unit_iso A)). + intro X. apply (invertible_2cell_to_nat_z_iso _ _ (left_equivalence_counit_iso 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.