Definition get_predoublecategory_interchange_comp {C : predoublecategory} {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 δ) := pr222 (pr222 (pr222 C)) a0 a1 a2 b0 b1 b2 c0 c1 c2 fa ga fb gb fc gc h0 k0 h1 k1 h2 k2 α β γ δ.
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.