fact: Definition is_z_isomorphism_identity {C : precategory} (c : C) : is_z_isomorphism (identity c).
imports: UniMath.Foundations.PartA UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories