Lemma folds_2_iso_implies_identity (a b : C) (f g : a ⇒ b) : folds_iso f g → f = g. Proof. intro Isofg. apply standardness. apply folds_iso_implies_E. apply Isofg. Qed.
Require Import UniMath.Folds.UnicodeNotations. Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets.