Lemma iseqrel_are_z_isomorphic {C : precategory} : iseqrel (are_z_isomorphic(C:=C)). 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.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories.