proposition: Lemma MonosAreInjective_HSET {A B : HSET} (f: HSET ⟦ A, B ⟧) : isMonic f ≃ isInjective f.
proof: 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.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Epis UniMath.CategoryTheory.Categories.HSET.Core