Definition make_predoublecategory_sq_hor_data (C : predoublecategory_ob_mor_sq_data) (id : (∏ (a b : C) (f: a -v-> b), (mor_sq C a a b b (hor_identity a) f f (hor_identity b)))) (comp: (∏ (a0 a1 b0 b1 c0 c1 : C) (f0: a0 -v-> a1) (f1: b0 -v-> b1) (f2: c0 -v-> c1) (g0: a0 -h-> b0) (h0: b0 -h-> c0) (g1: a1 -h-> b1) (h1: b1 -h-> c1), (sqq g0 f0 f1 g1) → (sqq h0 f1 f2 h1) → (sqq (g0 ·h h0) f0 f2 (g1 ·h h1))) ) : predoublecategory_sq_hor_data := tpair _ C (make_dirprod id comp).
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.