Lemma is_weq_precat_paths_to_iso_hset (A B : ob HSET): isweq (@idtoiso _ A B). Proof. rewrite hset_id_weq_iso_is. apply (pr2 (hset_id_weq_z_iso A B)). 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.