Definition predoublecategory_ver_assoc_coherence ( C : predoublecategory_sq_hor_ver_unit_assoc_data) : UU := ∏ (a b c d e: C) (f : a -v-> b) (g : b -v-> c) (h : c -v-> d) (k : d -v-> e), (hor_trans_id_right_sq ( (pr1 (get_ver_associator f g (h ·v k))) ·sqh (pr1 (get_ver_associator (f ·v g) h k)) )) = ( ( ( (hor_sq_identity f) ·sqv (pr1 (get_ver_associator g h k)) ) ·sqh (pr1 (get_ver_associator f (g ·v h) k)) ) ·sqh ( (pr1 (get_ver_associator f g h)) ·sqv (hor_sq_identity k)) ) .
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.