fact: 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) ).
imports: UniMath.Foundations.PartD UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.ProductCategory UniMath.CategoryTheory.HorizontalComposition UniMath.CategoryTheory.Equivalences.Core UniMath.Bicategories.WkCatEnrichment.prebicategory UniMath.Bicategories.WkCatEnrichment.whiskering UniMath.Bicategories.WkCatEnrichment.Notations