proposition: Lemma eq_iso {C: precategory_data} {a b : C} (f g : iso a b) : pr1 f = pr1 g -> f = g.
proof: Proof. intro H. apply subtypePath. - intros t. apply isaprop_is_iso. - apply H. Defined.
imports: UniMath.Foundations.PartA UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories