Definition strict_double_cat_assoc_square {C : category} {D : twosided_disp_cat C C} {Cm : hor_comp D} (ap : strict_double_cat_assoc Cm) : UU := ∏ (w₁ w₂ x₁ x₂ y₁ y₂ z₁ z₂ : C) (vw : w₁ --> w₂) (vx : x₁ --> x₂) (vy : y₁ --> y₂) (vz : z₁ --> z₂) (h₁ : D w₁ x₁) (h₂ : D x₁ y₁) (h₃ : D y₁ z₁) (k₁ : D w₂ x₂) (k₂ : D x₂ y₂) (k₃ : D y₂ z₂) (s₁ : h₁ -->[ vw ][ vx ] k₁) (s₂ : h₂ -->[ vx ][ vy ] k₂) (s₃ : h₃ -->[ vy ][ vz ] k₃), double_hor_comp_mor Cm s₁ (double_hor_comp_mor Cm s₂ s₃) = transportb_hor_mor (ap _ _ _ _ _ _ _) (ap _ _ _ _ _ _ _) (double_hor_comp_mor Cm (double_hor_comp_mor Cm s₁ s₂) s₃).
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Core.Setcategories. Require Import UniMath.CategoryTheory.Categories.CategoryOfSetCategories. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.DisplayedFunctor. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.DisplayedNatTrans. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Strictness. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TransportLaws. Require Import UniMath.Bicategories.DoubleCategories.Basics.DoubleCategoryBasics.