Lemma MonosAreInjective_HSET {A B : HSET} (f: HSET ⟦ A, B ⟧) : isMonic f ≃ isInjective f. Proof. apply weqimplimpl. - intro isM. apply incl_injectivity; intros b. apply invproofirrelevance; intros a1 a2. apply subtypePath; [intro; apply setproperty|]. apply global_element_HSET_paths_weq. apply isM. apply funextsec; intro t. abstract (induction t; exact (pr2 a1 @ ! pr2 a2)). - intro isI. unfold isMonic. intros ? ? ? eq. apply funextfun; intro. apply (invweq (Injectivity _ isI _ _)). apply toforallpaths in eq. apply eq. - apply isapropisMonic. - apply isaprop_isInjective. 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.