Definition idtoiso2 {C : folds_pre_2_cat} {a b : C} {f g : a ⇒ b} : f = g → folds_iso f g. Proof. destruct 1. exact (folds_2_iso_id _ _ _ f). Defined.
Require Import UniMath.Folds.UnicodeNotations. Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets.