Definition folds_2_iso_id (C : folds_pre_3_cat) (a b : C) (f : a ⇒ b) : folds_iso f f. Proof. repeat split; intros; apply idweq. Defined.
Require Import UniMath.Folds.UnicodeNotations. Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets.