proposition: Lemma iseqrel_are_z_isomorphic {C : precategory} : iseqrel (are_z_isomorphic(C:=C)).
proof: Proof. repeat split. - intros x y z h1. apply hinhuniv; intros h2; generalize h1; clear h1. now apply hinhuniv; intros h1; apply hinhpr, (z_iso_comp h1 h2). - now intros x; apply hinhpr, identity_z_iso. - now intros x y; apply hinhuniv; intro h1; apply hinhpr, z_iso_inv_from_z_iso. Qed.
imports: UniMath.Foundations.PartA UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories