Definition predoublecategory_sq_ver_id_comp (C : predoublecategory_hor_sq): UU := (∏ (a b : C) (f: a -h-> b), (sqq f (ver_identity a) (ver_identity b) f)) × (∏ (a0 a1 b0 b1 c0 c1 : C) (f0: a0 -h-> a1) (f1: b0 -h-> b1) (f2: c0 -h-> c1) (g0: a0 -v-> b0) (h0: b0 -v-> c0) (g1: a1 -v-> b1) (h1: b1 -v-> c1), (sqq f0 g0 g1 f1) → (sqq f1 h0 h1 f2) → (sqq f0 (g0 ·v h0) (g1 ·v h1) f2) ).
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.