Definition get_assoc_sq_hor (C : predoublecategory_hor_sq) : ∏ (a0 b0 c0 d0 a1 b1 c1 d1 : 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 γ) := pr222 C.
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.