A functor is additive iff...

Stream: Is there code for X?

[Adam Topaz]

I'm looking for the fact that a functor is additive if it preserves finite biproducts. I seem to recall @Scott Morrison proving this at some point, but I can't seem to find it right now...

[Adam Topaz]

Blah, ignore me, it's literally just docs#category_theory.functor.additive_of_preserves_binary_biproducts
sorry for the spam