Definition adj_int_equivalence {C : prebicategory} (a b : C) : UU := ∑ f : a -1-> b, is_adj_int_equivalence f. Local Definition identity_triangle1 {C : prebicategory} (a : C) : (inv (left_unitor (identity1 a))) ;v; (whisker_right (inv (left_unitor (identity1 a))) (identity1 a)) ;v; (inv (associator _ _ _)) ;v; (whisker_left (identity1 a) (right_unitor (identity1 a))) ;v; (right_unitor _) = identity (identity1 a). Proof. apply z_iso_inv_to_right. rewrite id_left. rewrite <- !assoc. apply z_iso_inv_on_right. intermediate_path (identity (identity1 a ;1; identity1 a)). { unfold inv ; cbn. rewrite whisker_right_inv. apply z_iso_inv_on_right. apply z_iso_inv_on_right. rewrite id_right. simpl. unfold whisker_left. unfold whisker_right. rewrite <- left_unitor_id_is_right_unitor_id. rewrite (triangle_axiom (identity1 a) (identity1 a)). rewrite <- left_unitor_id_is_right_unitor_id. reflexivity. } simpl. apply pathsinv0. rewrite left_unitor_id_is_right_unitor_id. apply (z_iso_inv_after_z_iso (right_unitor _)). Defined.
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.