Definition adj_equiv_is_equiv_cat {C D : bicat_of_univ_cats} (F : C --> D) : left_adjoint_equivalence F ≃ adj_equivalence_of_cats F. Proof. use make_weq. - exact (adj_equiv_to_equiv_cat F). - use isweq_iso. + exact (equiv_cat_to_adj_equiv F). + intros A. use subtypePath. * intro. do 2 apply isapropdirprod. ** apply cellset_property. ** apply cellset_property. ** apply isaprop_is_invertible_2cell. ** apply isaprop_is_invertible_2cell. * apply idpath. + intros A. use subtypePath. * intro. apply isapropdirprod ; apply impred ; intro ; apply isaprop_is_z_isomorphism. * use total2_paths_b. ** apply idpath. ** use subtypePath. *** intro ; simpl. apply (@isaprop_form_adjunction (pr1 C) (pr1 D)). *** apply idpath. 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.