fact: Definition make_predoublecategory_sq_hor_ver_data (C : predoublecategory_hor_sq) (id : (∏ (a b : C) (f: a -h-> b), (sqq f (ver_identity a) (ver_identity b) f))) (comp: (∏ (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)) ) : predoublecategory_sq_hor_ver_data := tpair _ C (make_dirprod id comp).
imports: UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Notations UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence