proposition: Lemma isaprop_is_z_isomorphism {C : category} {a b : ob C} (f : a --> b) : isaprop (is_z_isomorphism f).
proof: 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.
imports: UniMath.Foundations.PartA UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories