Lemma hset_z_iso_is_equiv (A B : ob HSET) (f : z_iso A B) : isweq (pr1 f). Proof. apply (isweq_iso _ (inv_from_z_iso f)). - intro x. set (T:=z_iso_inv_after_z_iso f). set (T':=toforallpaths _ _ _ T). apply T'. - intro x. apply (toforallpaths _ _ _ (z_iso_after_z_iso_inv f)). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Epis. Require Import UniMath.CategoryTheory.Categories.HSET.Core.