Definition adjoint_equivalence_is_weq {X Y : one_types} (f : one_types⟦X,Y⟧) (Hf : left_adjoint_equivalence f) : isweq f. Proof. use isweq_iso. - exact (left_adjoint_right_adjoint Hf). - intros x. exact (!left_adjoint_unit Hf x). - intros x. exact (left_adjoint_counit Hf x). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.Core.AdjointUnique.