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