Definition adj_equivalence_from_right_adjoint {A B : category} (F : functor A B) (H1 : is_right_adjoint F) (H2 : ∏ a, is_z_isomorphism ((unit_from_right_adjoint H1) a)) (H3 : ∏ a, is_z_isomorphism ((counit_from_right_adjoint H1) a)) : adj_equivalence_of_cats F := make_adj_equivalence_of_cats' F (left_adjoint H1) (unit_from_right_adjoint H1) (counit_from_right_adjoint H1) (pr2 (pr2 H1)) H2 H3.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Adjunctions.Core.