noncomputable def ext0_addEquiv_hom (R : Type u) [Ring R] [Small.{v, u} R] (M A : ModuleCat R) : ExtGroup_R R M A 0 ≃+ (M ⟶ A)