Definition double_associator_laws {C : category} {D : twosided_disp_cat C C} {Cm : hor_comp D} (a : double_associator_data Cm) : UU := ∏ (w₁ w₂ x₁ x₂ y₁ y₂ z₁ z₂ : C) (h₁ : D w₁ x₁) (h₂ : D w₂ x₂) (j₁ : D x₁ y₁) (j₂ : D x₂ y₂) (k₁ : D y₁ z₁) (k₂ : D y₂ z₂) (vw : w₁ --> w₂) (vx : x₁ --> x₂) (vy : y₁ --> y₂) (vz : z₁ --> z₂) (τ₁ : h₁ -->[ vw ][ vx ] h₂) (τ₂ : j₁ -->[ vx ][ vy ] j₂) (τ₃ : k₁ -->[ vy ][ vz ] k₂), transportb_disp_mor2 (id_right _ @ !(id_left _)) (id_right _ @ !(id_left _)) (a _ _ _ _ h₁ j₁ k₁ ;;2 double_hor_comp_mor Cm (double_hor_comp_mor Cm τ₁ τ₂) τ₃) = double_hor_comp_mor Cm τ₁ (double_hor_comp_mor Cm τ₂ τ₃) ;;2 a _ _ _ _ h₂ j₂ k₂.
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.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos.