Definition adj_equiv (A B : category) : UU := ∑ F : functor A B, adj_equivalence_of_cats F. Coercion left_adjequiv (A B : category) (F : adj_equiv A B) : functor A B := pr1 F. Coercion adj_equiv_of_cats_from_adj {A B : category} (E : adj_equiv A B) : adj_equivalence_of_cats E := pr2 E. Coercion adj_from_adj_equiv {A B} (F : adj_equiv A B) : adjunction A B. Proof. use make_adjunction. use(make_adjunction_data F). - exact(right_adjoint F). - exact(adjunit F). - exact(adjcounit F). - use make_form_adjunction. + apply triangle_id_left_ad. + apply triangle_id_right_ad. Defined.
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.