Lemma hset_equiv_is_z_iso (A B : hSet) (f : (pr1 A) ≃ (pr1 B)) : is_z_isomorphism (C:=HSET) (pr1 f). Proof. exists (invmap f). split; simpl. - apply funextfun; intro x; simpl in *. unfold compose, identity; simpl. apply homotinvweqweq. - apply funextfun; intro x; simpl in *. unfold compose, identity; simpl. apply homotweqinvweq. 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.