Definition is_predoublecategory_hor_sq (C : predoublecategory_sq_hor_data) : UU := ((∏ (a b c d : C) (f: a -h-> b) (g: a -v-> c) (h: b -v-> d) (k: c -h-> d) (α : mor_sq C a b c d f g h k), (hor_sq_identity g) ·sqh α = hor_trans_id_left_sq α)) × ((∏ (a b c d : C) (f: a -h-> b) (g: a -v-> c) (h: b -v-> d) (k: c -h-> d) (α : mor_sq C a b c d f g h k), α ·sqh (hor_sq_identity h) = hor_trans_id_right_sq α)) × (∏ ( a0 b0 c0 d0 a1 b1 c1 d1 : C ) (f0: a0 -h-> b0) (g0: b0 -h-> c0) (h0: c0 -h-> d0) (f1: a1 -h-> b1) (g1: b1 -h-> c1) (h1: c1 -h-> d1) (ma: a0 -v-> a1) (mb: b0 -v-> b1) (mc: c0 -v-> c1) (md: d0 -v-> d1) (α: sqq f0 ma mb f1) (β: sqq g0 mb mc g1) (γ: sqq h0 mc md h1), α ·sqh (β ·sqh γ) = hor_trans_assoc_sq ((α ·sqh β) ·sqh γ)) .
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.