Lemma EpisAreSurjective_HSET {A B : HSET} (f: HSET ⟦ A, B ⟧) : isEpi f ≃ issurjective f. Proof. apply weqimplimpl. - intro epif. apply epiissurjectiontosets; [apply setproperty|]. intros ? ? ? ?. apply toforallpaths. apply epif. now apply funextfun. - intros is_surj_f. intros C g h H. apply funextfun; intro. specialize (is_surj_f x). apply (squash_to_prop is_surj_f); [apply setproperty|]. intro x'. refine (!maponpaths _ (hfiberpr2 _ _ x') @ _). refine (_ @ maponpaths _ (hfiberpr2 _ _ x')). apply toforallpaths in H. apply H. - apply isapropisEpi. apply has_homsets_HSET. - apply isapropissurjective. Qed.
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.