Definition isotoid2 (C : folds_pre_2_cat) (H : is_univalent_folds_pre_2_cat C) (a b : C) (f g : a ⇒ b) : folds_iso f g → f = g := invmap (make_weq _ (H a b f g)).
Require Import UniMath.Folds.UnicodeNotations. Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets.