Definition predoublecategory_interchange_comp ( C : predoublecategory_sq_hor_ver_unit_assoc_data) : UU := ∏ (a0 a1 a2 b0 b1 b2 c0 c1 c2 : C) (fa: a0 -h-> a1) (ga: a1 -h-> a2) (fb: b0 -h-> b1) (gb: b1 -h-> b2) (fc: c0 -h-> c1) (gc: c1 -h-> c2) (h0: a0 -v-> b0) (k0: b0 -v-> c0) (h1: a1 -v-> b1) (k1: b1 -v-> c1) (h2: a2 -v-> b2) (k2: b2 -v-> c2) (α : sqq fa h0 h1 fb) (β : sqq ga h1 h2 gb) (γ : sqq fb k0 k1 fc) (δ : sqq gb k1 k2 gc), (α ·sqh β) ·sqv (γ ·sqh δ) = (α ·sqv γ) ·sqh (β ·sqv δ).
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.