Conflicting zero objects for Module R

Stream: new members

[Amelia Livingston]

Posting in new members because I doubt this is an interesting question, but I'm getting conflicts between abelian.has_zero_object and Module.category_theory.limits.has_zero_object:

import category_theory.abelian.ext
import algebra.category.Module.projective

universes u

variables {R : Type u} [ring R]

open category_theory

instance : has_projective_resolutions (Module.{u} R) :=
@ProjectiveResolution.category_theory.has_projective_resolutions
  (Module.{u} R) _ _ Module.Module_enough_projectives.{u}

I got round it for a short while by giving abelian.has_zero_object as an argument to has_projective_resolutions but now I've run into later conflicts.

[Adam Topaz]

Maybe we should change has_zero_object to be a Prop?