Definition is_adj_int_equivalence {C : prebicategory} { a b : C } (f : a -1-> b) := ∑ (g : b -1-> a) (etaeps : (z_iso (identity1 a) (f ;1; g)) × (z_iso (g ;1; f) (identity1 b))), let eta := pr1 etaeps in let eps := pr2 etaeps in ( (inv (left_unitor f)) ;v; (whisker_right eta f) ;v; (inv (associator _ _ _)) ;v; (whisker_left f eps) ;v; (right_unitor _) = (identity f) ) × ( (inv (right_unitor g)) ;v; (whisker_left g eta) ;v; (associator _ _ _) ;v; (whisker_right eps g) ;v; (left_unitor _) = (identity g) ).
Require Import UniMath.Foundations.PartD. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.ProductCategory. Require Import UniMath.CategoryTheory.HorizontalComposition. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.Bicategories.WkCatEnrichment.prebicategory. Require Import UniMath.Bicategories.WkCatEnrichment.whiskering. Require Import UniMath.Bicategories.WkCatEnrichment.Notations.