Definition disp_invertible_2cell_rwhisker {B : bicat} {x y z : B} {f₁ f₂ : x --> y} {g : y --> z} {α : invertible_2cell f₁ f₂} {D : disp_bicat B} {xx : D x} {yy : D y} {zz : D z} {ff₁ : xx -->[f₁] yy} {ff₂ : xx -->[f₂] yy} (gg : yy -->[g] zz) (αα : disp_invertible_2cell α ff₁ ff₂) : disp_invertible_2cell (_ ,, is_invertible_2cell_rwhisker g (pr2 α)) _ _ := disp_rwhisker gg αα,, is_disp_invertible_2cell_rwhisker gg αα.
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.