Lemma is_folds_precat_implies_is_univalent : is_univalent_folds_pre_2_cat C. Proof. intros a b f g. apply isweqimplimpl. - apply folds_2_iso_implies_identity. - apply (pr1 H). - apply isaprop_folds_2_iso. Qed.
Require Import UniMath.Folds.UnicodeNotations. Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets.