Definition is_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₂) : is_disp_invertible_2cell (is_invertible_2cell_rwhisker g (pr2 α)) (αα ▹▹ gg). Proof. use tpair. - exact (disp_inv_cell αα ▹▹ gg). - split. + abstract (refine (disp_rwhisker_vcomp _ _ @ _) ; refine (maponpaths _ (maponpaths _ (disp_vcomp_rinv _)) @ _) ; unfold transportb ; rewrite disp_rwhisker_transport_left_new ; rewrite disp_id2_rwhisker ; unfold transportb ; rewrite !transport_f_f ; apply (transportf_paths (λ p, _ ==>[ p ] _)) ; apply B). +abstract (refine (disp_rwhisker_vcomp _ _ @ _) ; refine (maponpaths _ (maponpaths _ (disp_vcomp_linv _)) @ _) ; unfold transportb ; rewrite disp_rwhisker_transport_left_new ; rewrite disp_id2_rwhisker ; unfold transportb ; rewrite !transport_f_f ; apply (transportf_paths (λ p, _ ==>[ p ] _)) ; apply B). 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.