Definition discrete_fiber_lassociator {d0 d1 d2 d3 : D c} (ff : d0 -->[ id₁ c] d1) (gg : d1 -->[ id₁ c] d2) (hh : d2 -->[ id₁ c] d3) : local_iso_cleaving_1cell h (ff;; local_iso_cleaving_1cell h (gg;; hh) (idempunitor c)) (idempunitor c) ==>[ id₂ (id₁ c)] local_iso_cleaving_1cell h (local_iso_cleaving_1cell h (ff;; gg) (idempunitor c);; hh) (idempunitor c). Proof. assert ((idempunitor c • (identity c ◃ idempunitor c)) • lassociator _ _ _ • ((lunitor _ ▹ identity c) • lunitor _) = id2 _) as Heq. { abstract (cbn ; rewrite !lwhisker_hcomp, !rwhisker_hcomp ; rewrite !vassocl ; rewrite !(maponpaths (λ z, _ • (_ • z)) (vassocr _ _ _)) ; rewrite triangle_r_inv ; rewrite !vassocl ; rewrite !(maponpaths (λ z, _ • (_ • z)) (vassocr _ _ _)) ; rewrite rassociator_lassociator, id2_left ; rewrite !(maponpaths (λ z, _ • z) (vassocr _ _ _)) ; rewrite <- hcomp_vcomp ; rewrite <- lunitor_V_id_is_left_unit_V_id ; rewrite id2_left, linvunitor_lunitor ; rewrite hcomp_identity, id2_left ; apply linvunitor_lunitor ). } refine (transportf (λ z, _ ==>[ z ] _) Heq _). cbn. refine (_ •• disp_lassociator ff gg hh •• _). - refine (_ •• _). + exact (disp_local_iso_cleaving_invertible_2cell h (ff;;local_iso_cleaving_1cell h (gg;; hh) (idempunitor c)) (idempunitor c)). + refine (disp_lwhisker _ _). exact (disp_local_iso_cleaving_invertible_2cell h (gg ;; hh) (idempunitor c)). - refine (_ •• _). + refine (disp_rwhisker _ _). exact (disp_inv_cell (disp_local_iso_cleaving_invertible_2cell h (ff ;; gg) (idempunitor c))). + exact (disp_inv_cell (disp_local_iso_cleaving_invertible_2cell h (local_iso_cleaving_1cell h (ff;; gg) (idempunitor c);; hh) (idempunitor c))). 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.