Lemma isaprop_is_z_isomorphism {C : category} {a b : ob C} (f : a --> b) : isaprop (is_z_isomorphism f). Proof. apply invproofirrelevance. intros g g'. set (Hpr1 := inverse_unique_precat _ _ _ _ _ (pr2 g) (pr2 g')). apply (total2_paths_f Hpr1). destruct g as [g [eta eps]]. destruct g' as [g' [eta' eps']]. simpl in *. apply isapropdirprod; apply homset_property. 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.