Lemma isaprop_folds_ax_id C : isaprop (folds_ax_I C). Proof. repeat (apply isapropdirprod). - apply impred; intro; apply isapropishinh. - repeat (apply impred; intro). apply pr2. - repeat (apply impred; intro). apply pr2. Qed.
Require Import UniMath.Folds.UnicodeNotations. Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets.