Definition transport_along_inv_2cell_disp_invertible_2cell {B : bicat} (HB : is_univalent_2_1 B) {D : disp_bicat B} {x y : B} {f g : x --> y} (α : invertible_2cell f g) {xx : D x} {yy : D y} (ff : xx -->[ f ] yy) : disp_invertible_2cell (inv_of_invertible_2cell α) (transport_along_inv_2cell HB α ff) ff. Proof. refine (transportf (λ z, disp_invertible_2cell z _ _) _ (transport_1cell_disp_invertible_2cell (isotoid_2_1 HB α) ff)). abstract (use subtypePath ; [ intro ; apply isaprop_is_invertible_2cell | ] ; cbn ; rewrite idtoiso_2_1_isotoid_2_1 ; apply idpath). 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.CategoryTheory.DisplayedCats.Isos. 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.Invertible_2cells.