Definition is_univalent_folds_pre_2_cat (C : folds_pre_2_cat) : UU := ∏ (a b : C) (f g : a ⇒ b), isweq (@idtoiso2 _ _ _ f g).
Require Import UniMath.Folds.UnicodeNotations. Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets.