Definition predoublecategory_interchange_id_hor ( C : predoublecategory_sq_hor_ver_unit_assoc_data) : UU := ∏ (a b c: C) (f: a -h-> b) (g: b -h-> c), ver_sq_identity(f ·h g) = (ver_sq_identity f) ·sqh (ver_sq_identity g).
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.