proposition: Lemma isaprop_folds_2_iso (C : folds_pre_2_cat) (a b : C) (f g : a ⇒ b) : isaprop (folds_iso f g).
proof: Proof. repeat (apply isofhleveldirprod); repeat (apply impred; intro); apply isofhlevelsnweqtohlevelsn; folds_pre_2_cat_props C. Qed.
imports: UniMath.Folds.UnicodeNotations UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets