Definition inv2cell_to_disp_adj_equiv_disp_end {x : B} {ex ey : disp_end x} (τ : invertible_2cell ex ey) : disp_adjoint_equivalence (internal_adjoint_equivalence_identity x) ex ey. Proof. simple refine (_ ,, ((_ ,, (_ ,, _)) ,, ((_ ,, _) ,, (_ ,, _)))). - exact (lunitor _ • τ^-1 • rinvunitor _). - exact (lunitor _ • τ • rinvunitor _). - abstract (cbn ; rewrite <- !lwhisker_vcomp ; rewrite <- !rwhisker_vcomp ; rewrite !vassocr ; rewrite <- linvunitor_assoc ; refine (!_) ; rewrite lwhisker_hcomp ; rewrite <- linvunitor_natural ; rewrite !vassocl ; apply maponpaths ; rewrite !rwhisker_hcomp ; rewrite <- triangle_r_inv ; rewrite <- !lwhisker_hcomp ; rewrite <- !rwhisker_hcomp ; rewrite !vassocr ; apply maponpaths_2 ; rewrite !vassocl ; etrans ; [ do 3 apply maponpaths ; rewrite !vassocr ; rewrite lunitor_triangle ; apply idpath | ] ; etrans ; [ do 2 apply maponpaths ; rewrite !vassocr ; rewrite vcomp_lunitor ; rewrite !vassocl; rewrite rwhisker_hcomp ; rewrite <- rinvunitor_natural ; apply idpath | ] ; rewrite !vassocr ; refine (_ @ id2_left _) ; apply maponpaths_2 ; use vcomp_move_R_Mp ; [ is_iso | ] ; cbn ; rewrite !vassocl ; use vcomp_move_R_pM ; [ is_iso | ] ; cbn ; rewrite id2_left ; rewrite vcomp_lunitor ; apply idpath). - abstract (cbn ; rewrite <- !lwhisker_vcomp ; rewrite <- !rwhisker_vcomp ; rewrite !vassocr ; rewrite lunitor_lwhisker ; rewrite runitor_lunitor_identity ; rewrite !vassocl ; apply maponpaths ; rewrite lunitor_lwhisker ; rewrite rwhisker_vcomp ; rewrite rinvunitor_runitor ; rewrite id2_rwhisker ; rewrite id2_right ; use vcomp_move_R_pM ; [ is_iso | ] ; cbn ; rewrite !vassocr ; rewrite rinvunitor_triangle ; rewrite rwhisker_hcomp ; rewrite <- rinvunitor_natural ; rewrite vcomp_lunitor ; rewrite !vassocl ; apply maponpaths ; rewrite rinvunitor_natural ; rewrite <- rwhisker_hcomp ; apply idpath). - apply disp_2cells_isaprop_end_bicat. - apply disp_2cells_isaprop_end_bicat. - apply disp_locally_groupoid_end_bicat. - apply disp_locally_groupoid_end_bicat. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence.