Definition identity_adj_int_equivalence {C : prebicategory} (a : C) : adj_int_equivalence a a. Proof. exists (identity1 a). exists (identity1 a). use tpair. - exists (inv (left_unitor (identity1 a))). exact (right_unitor (identity1 a)). - split. + apply identity_triangle1. + apply identity_triangle2. 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.