Definition assoc_sq_hor {C : predoublecategory_hor_sq} {a0 b0 c0 d0 a1 b1 c1 d1 : pr1 C} {f0: a0 -h-> b0} {g0: b0 -h-> c0} {h0: c0 -h-> d0} {f1: a1 -h-> b1} {g1: b1 -h-> c1} {h1: c1 -h-> d1} {ma: a0 -v-> a1} {mb: b0 -v-> b1} {mc: c0 -v-> c1} {md: d0 -v-> d1} (α: sqq f0 ma mb f1) (β: sqq g0 mb mc g1) (γ: sqq h0 mc md h1) : α ·sqh (β ·sqh γ) =hor_trans_assoc_sq ( (α ·sqh β) ·sqh γ) := get_assoc_sq_hor C a0 b0 c0 d0 a1 b1 c1 d1 f0 g0 h0 f1 g1 h1 ma mb mc md α β γ.
Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence.