proposition: Lemma z_iso_inv_z_iso_inv {C : category} (a b : ob C) (f : z_iso a b) : z_iso_inv_from_z_iso (z_iso_inv_from_z_iso f) = f.
proof: Proof. apply z_iso_eq. apply idpath. Defined.
imports: UniMath.Foundations.PartA UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories