proposition: Lemma eq_idtoiso_idtomor {C:precategory} (a b:ob C) (e:a = b) : pr1 (idtoiso e) = idtomor _ _ e.
proof: Proof. destruct e; reflexivity. Defined.
imports: UniMath.Foundations.PartA UniMath.Foundations.Sets UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos