Lemma InjectivesAreMonic_type {A B : UU} (f: type_precat⟦ A, B ⟧) : isInjective f -> isMonic f. Proof. intro isI. unfold isMonic. intros ? ? ? eq. apply funextfun; intro. apply (invweq (Injectivity _ isI _ _)). apply toforallpaths in eq. apply eq. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Epis. Require Import UniMath.CategoryTheory.Categories.Type.Core.