Lemma isaprop_is_folds_precategory (C : folds_pre_2_cat) : isaprop (is_folds_precategory C). Proof. apply isofhlevelsn. intro H. repeat (apply isofhleveldirprod). - do 2 (apply impred; intro). apply isapropisaset. - do 9 (apply impred; intro). apply (pr1 H). - do 15 (apply impred; intro). apply H. Qed.
Require Import UniMath.Folds.UnicodeNotations. Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets.