Definition is_disp_invertible_2cell_rassociator {B : bicat} {w x y z : B} {f : w --> x} {g : x --> y} {h : y --> z} {D : disp_bicat B} {ww : D w} {xx : D x} {yy : D y} {zz : D z} (ff : ww -->[f] xx) (gg : xx -->[g] yy) (hh : yy -->[h] zz) : is_disp_invertible_2cell (is_invertible_2cell_rassociator f g h) (disp_rassociator ff gg hh). Proof. use tpair. - exact (disp_lassociator ff gg hh). - split. + etrans. { apply disp_rassociator_lassociator. } apply (transportf_paths (λ p, _ ==>[p] _)). apply B. + etrans. { apply disp_lassociator_rassociator. } 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.