Definition discrete_fiber_lassociator_disp_invertible {d0 d1 d2 d3 : D c} (ff : d0 -->[ id₁ c] d1) (gg : d1 -->[ id₁ c] d2) (hh : d2 -->[ id₁ c] d3) : disp_invertible_2cell (id2_invertible_2cell (id₁ c)) (local_iso_cleaving_1cell h (ff;; local_iso_cleaving_1cell h (gg;; hh) (idempunitor c)) (idempunitor c)) (local_iso_cleaving_1cell h (local_iso_cleaving_1cell h (ff;; gg) (idempunitor c);; hh) (idempunitor c)). Proof. use tpair. - exact (discrete_fiber_lassociator ff gg hh). - use tpair. + exact (discrete_fiber_rassociator ff gg hh). + abstract (split ; apply HD). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence. Require Import UniMath.Bicategories.DisplayedBicats.DispInvertibles. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.DisplayedBicats.CleavingOfBicat.