Definition is_folds_pre_2_cat (C : folds_pre_3_cat) := ( (∏ (a : C) (i : a ⇒ a), isaprop (I i)) × (∏ (a b c : C) (f : a ⇒ b) (g : b ⇒ c) (h : a ⇒ c), isaprop (T f g h))) × (∏ (a b : C) (f g : a ⇒ b), isaprop (E f g)).
Require Import UniMath.Folds.UnicodeNotations. Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets.