Definition disp_adj_equiv_to_inv2cell_disp_end {x : B} {ex ey : disp_end x} (τ : disp_adjoint_equivalence (internal_adjoint_equivalence_identity x) ex ey) : invertible_2cell ex ey. Proof. use make_invertible_2cell. - exact (linvunitor _ • pr112 τ • runitor _). - use make_is_invertible_2cell. + exact (linvunitor _ • pr1 τ • runitor _). + abstract (rewrite !vassocl ; use vcomp_move_R_pM ; [ is_iso | ] ; cbn ; rewrite !vassocr ; use vcomp_move_R_Mp ; [ is_iso | ] ; cbn ; rewrite id2_right ; use (vcomp_rcancel (ex ◃ linvunitor _)) ; [ is_iso | ] ; refine (_ @ !(pr1 (pr212 τ))) ; cbn ; rewrite !vassocr ; rewrite <- linvunitor_assoc ; refine (!_) ; rewrite lwhisker_hcomp ; rewrite <- linvunitor_natural ; rewrite !vassocl ; apply maponpaths ; rewrite linvunitor_assoc ; rewrite !vassocl ; rewrite (maponpaths (λ z, _ • z) (vassocr _ _ _)) ; rewrite rassociator_lassociator ; rewrite id2_left ; rewrite !vassocr ; rewrite <- vcomp_runitor ; rewrite !vassocl ; apply maponpaths ; rewrite !vassocr ; rewrite <- vcomp_runitor ; rewrite !vassocl ; apply maponpaths ; rewrite <- runitor_triangle ; rewrite runitor_lunitor_identity ; rewrite !vassocl ; rewrite lwhisker_vcomp ; rewrite lunitor_linvunitor ; rewrite lwhisker_id2 ; rewrite id2_right ; apply idpath). + abstract (rewrite !vassocl ; use vcomp_move_R_pM ; [ is_iso | ] ; cbn ; rewrite !vassocr ; use vcomp_move_R_Mp ; [ is_iso | ] ; cbn ; rewrite id2_right ; use (vcomp_lcancel (lunitor _ ▹ ey)) ; [ is_iso | ] ; refine (_ @ pr2 (pr212 τ)) ; cbn ; rewrite !vassocl ; use vcomp_move_L_pM ; [ is_iso | ] ; cbn ; rewrite !vassocr ; rewrite lunitor_triangle ; rewrite <- vcomp_lunitor ; rewrite !vassocl ; apply maponpaths ; rewrite lunitor_runitor_identity ; rewrite runitor_triangle ; rewrite vcomp_runitor ; rewrite !vassocr ; apply maponpaths_2 ; rewrite !vassocl ; rewrite <- vcomp_runitor ; rewrite !vassocr ; apply maponpaths_2 ; use vcomp_move_R_Mp ; [ is_iso | ] ; cbn ; rewrite lunitor_triangle ; apply idpath). 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.