proposition: Lemma weq_iff_z_iso_SET {X Y:HSET} (f:X-->Y) : is_z_isomorphism f <-> isweq f.
proof: 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.
imports: UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.yoneda UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.MonoEpiIso UniMath.Foundations.Preamble UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics