Lemma isaprop_folds_ax_T (C:folds_id_T) (hs: has_folds_homsets C): isaprop (folds_ax_T C). Proof. repeat (apply isapropdirprod). - do 5 (apply impred; intro). apply isapropishinh. - repeat (apply impred; intro). apply hs. - repeat (apply impred; intro). apply hs. Qed.
Require Import UniMath.Folds.UnicodeNotations. Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets.