fact: Definition get_predoublecategory_ver_assoc_naturality {C : predoublecategory} {a0 a1 a2 a3 b0 b1 b2 b3 : C} {fa: a0 -v-> a1} {fb: b0 -v-> b1} {ha: a1 -v-> a2} {hb: b1 -v-> b2} {ka: a2 -v-> a3} {kb: b2 -v-> b3} {g0: a0 -h-> b0} {g1: a1 -h-> b1} {g2: a2 -h-> b2} {g3: a3 -h-> b3} (α : sqq g0 fa fb g1) (β : sqq g1 ha hb g2) (γ : sqq g2 ka kb g3) : ( ( (α) ·sqv ( (β) ·sqv (γ)) ) ·sqh (pr1 (get_ver_associator fb hb kb)) = boundary_sq_transport (id_hor_right _ @ !(id_hor_left _)) (id_hor_right _ @ !(id_hor_left _)) ((pr1 (get_ver_associator fa ha ka)) ·sqh ( (α ·sqv β) ·sqv (γ) )) ) := (pr1 (pr222 C)) a0 a1 a2 a3 b0 b1 b2 b3 fa fb ha hb ka kb g0 g1 g2 g3 α β γ.
imports: UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Notations UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence