Definition section_disp_bicat_laws_lassociator {B : bicat} {D : disp_bicat B} (s : section_disp_bicat_data D) := ∏ (w x y z : B) (f : w --> x) (g : x --> y) (h : y --> z), transportf (λ z, _ ==>[ z ] _) (section_disp_bicat_laws_lassociator_base f g h) (((section_on_mor s f ◃◃ pr1 (section_on_comp s g h)) •• pr1 (section_on_comp s f (g · h))) •• section_on_cell s (lassociator f g h)) = (disp_lassociator (section_on_mor s f) (section_on_mor s g) (section_on_mor s h) •• (pr1 (section_on_comp s f g) ▹▹ section_on_mor s h)) •• pr1 (section_on_comp s (f · g) h).
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.Core.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.DispInvertibles. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor.