Definition transportf_is_disp_invertible_2cell {B : bicat} {D : disp_bicat B} {x y : B} {f g : x --> y} {α β : f ==> g} (Hα : is_invertible_2cell α) (Hβ : is_invertible_2cell β) {xx : D x} {yy : D y} {ff : xx -->[ f ] yy} {gg : xx -->[ g ] yy} {αα : ff ==>[ α ] gg} (p : α = β) (Hαα : is_disp_invertible_2cell Hα αα) : is_disp_invertible_2cell Hβ (transportf (λ z, _ ==>[ z ] _) p αα). Proof. induction p ; cbn. refine (transportf (λ z, is_disp_invertible_2cell z αα) _ Hαα). apply isaprop_is_invertible_2cell. 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.