When does a functor preserve finite (co)limits?

Stream: Is there code for X?

[Jujian Zhang]

Do we have that if a functor between abelian categories preserves terminal object, binary products, equalizers, then it preserves all finite limits, i.e. 0035 from stack?

[Adam Topaz]

we should

[Adam Topaz]

https://leanprover-community.github.io/mathlib_docs/category_theory/limits/constructions/finite_products_of_binary_products.html

[Markus Himmel]

We are about to get a much stronger statement: a functor between additive categories that preserves kernels preserves finite limits (note that the functor does not need to be additive). @Jakob von Raumer did this for abelian categories in #14026 and he will be able to generalize it to additive categories once #14452 is merged.