Lemma weq_iff_z_iso_SET {X Y:HSET} (f:X-->Y) : is_z_isomorphism f <-> isweq f. Proof. split. - intro i. set (F := make_z_iso' f i). refine (isweq_iso f (inv_from_z_iso F) (λ x, eqtohomot (z_iso_inv_after_z_iso F) x) (λ y, eqtohomot (z_iso_after_z_iso_inv F) y)). - intro i. apply (hset_equiv_is_z_iso X Y (_,,i)). Defined.
Require Import UniMath.MoreFoundations.Tactics.