Definition is_folds_precategory (C : folds_pre_2_cat) : UU := (∏ a b : C, isaset (a ⇒ b)) × ((∏ (a b c : C) (f : a ⇒ b) (g : b ⇒ c) (h k : a ⇒ c), T f g h → T f g k → h = k ) × (∏ (a b c d : C) (f : a ⇒ b) (g : b ⇒ c) (h : c ⇒ d) (fg : a ⇒ c) (gh : b ⇒ d) (fg_h : a ⇒ d) (f_gh : a ⇒ d), T f g fg → T g h gh → T fg h fg_h → T f gh f_gh → f_gh = fg_h)).
Require Import UniMath.Folds.UnicodeNotations. Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets.