Definition hor_trans_assoc_sq {C : predoublecategory_sq_hor_data} { 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} {md: d0 -v-> d1} (α: sqq ((f0 ·h g0) ·h h0) ma md ((f1 ·h g1) ·h h1)): sqq (f0 ·h (g0 ·h h0)) ma md (f1 ·h (g1 ·h h1)) := boundary_sq_transport (assoc_hor f0 g0 h0) (assoc_hor f1 g1 h1) α.
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.