abelian sheaves

Stream: condensed mathematics

[Johan Commelin]

We'll need to know that sheaves of abelian groups are the same as abelian group objects in sheaves of sets/types. I'll try to do this today/tomorrow.

[Adam Topaz]

I think docs#category_theory.presheaf.is_sheaf_iff_is_sheaf_forget should be useful for this.