Definition is_disp_invertible_2cell_lassociator {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_lassociator f g h) (disp_lassociator ff gg hh). Proof. use tpair. - exact (disp_rassociator ff gg hh). - split. + etrans. { apply disp_lassociator_rassociator. } apply (transportf_paths (λ p, _ ==>[p] _)). apply B. + etrans. { apply disp_rassociator_lassociator. } 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.