Lemma folds_iso_implies_E (C : folds_pre_2_cat) (a b : C) (f g : a ⇒ b) : folds_iso f g → E f g. Proof. intro Isofg. set (keytojoy := pr1 (pr2 (pr2 (pr2 Isofg)))). apply (keytojoy f). set (H' := pr2 (pr2 (pr1 C))). simpl in H'. destruct H' as [[[Erefl Esym] Etrans] [EI ET]]. apply Erefl. Qed.
Require Import UniMath.Folds.UnicodeNotations. Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets.