Definition assoc_two_disp_law (D : twosided_disp_cat_data) : UU := ∏ (x₁ x₂ x₃ x₄ : C₁) (y₁ y₂ y₃ y₄ : C₂) (xy₁ : D x₁ y₁) (xy₂ : D x₂ y₂) (xy₃ : D x₃ y₃) (xy₄ : D x₄ y₄) (f₁ : x₁ --> x₂) (f₂ : x₂ --> x₃) (f₃ : x₃ --> x₄) (g₁ : y₁ --> y₂) (g₂ : y₂ --> y₃) (g₃ : y₃ --> y₄) (fg₁ : xy₁ -->[ f₁ ][ g₁ ] xy₂) (fg₂ : xy₂ -->[ f₂ ][ g₂ ] xy₃) (fg₃ : xy₃ -->[ f₃ ][ g₃ ] xy₄), (fg₁ ;;2 (fg₂ ;;2 fg₃)) = transportb_disp_mor2 (assoc _ _ _) (assoc _ _ _) ((fg₁ ;;2 fg₂) ;;2 fg₃).
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.PrecategoryBinProduct.