Lemma isaprop_is_univalent_folds_2_precat (C : folds_pre_2_cat) : isaprop (is_univalent_folds_pre_2_cat C). Proof. do 4 (apply impred; intro); apply isapropisweq. Qed.
Require Import UniMath.Folds.UnicodeNotations. Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets.