Definition disp_identity_adjoint_equivalence {C : bicat} {D : disp_bicat C} {a : C} (aa : D a) : disp_adjoint_equivalence (internal_adjoint_equivalence_identity a) aa aa. Proof. use tpair. - apply disp_internal_adjunction_data_identity. - cbn. use tpair. + apply disp_internal_adjunction_data_identity. + cbn. split. { apply is_disp_internal_adjunction_identity. } { split. - use tpair. + apply disp_lunitor. + split. * cbn. refine (disp_linvunitor_lunitor (id_disp aa) @ _). apply (@transportf_paths _ (λ z, _ ==>[ z ] _)). apply C. * cbn. refine (disp_lunitor_linvunitor (id_disp aa) @ _). apply (@transportf_paths _ (λ z, _ ==>[ z ] _)). apply C. - use tpair. + apply disp_linvunitor. + split. * cbn. refine (disp_lunitor_linvunitor (id_disp aa) @ _). apply (@transportf_paths _ (λ z, _ ==>[ z ] _)). apply C. * cbn. refine (disp_linvunitor_lunitor (id_disp aa) @ _). apply (@transportf_paths _ (λ z, _ ==>[ z ] _)). apply C. } Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.DisplayedBicats.DispInvertibles. Require Import UniMath.Bicategories.Core.Univalence.