Lemma folds_iso_eq {a b : C} (i i' : folds_iso a b) : folds_iso_data_from_folds_iso i = folds_iso_data_from_folds_iso i' → i = i'. Proof. intro H. apply subtypePath. - intro; apply isaprop_folds_iso_prop. - assumption. Qed.
Require Import UniMath.Folds.UnicodeNotations. Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.Folds.folds_precat. Require Import UniMath.Folds.from_precats_to_folds_and_back.