Lemma hset_id_weq_iso_is (A B : ob HSET): @idtoiso _ A B = pr1 (hset_id_weq_z_iso A B). Proof. apply funextfun. intro p; elim p. apply z_iso_eq; simpl. - apply funextfun; intro x; destruct A. apply idpath. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.Foundations.HLevels. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Categories.HSET.MonoEpiIso.