Lemma weq_to_iso_SET {X Y:HSET} : z_iso X Y ≃ ((X:hSet) ≃ (Y:hSet)). Proof. intros. apply weqfibtototal; intro f. apply weqiff. - apply weq_iff_z_iso_SET. - apply isaprop_is_z_isomorphism. - apply isapropisweq. Defined.
Require Import UniMath.MoreFoundations.Tactics.