mathlib3

bbe25d4d - feat(category_theory): left-exact functors preserve finite limits (#14026)

feat(category_theory): left-exact functors preserve finite limits (#14026) Also adds the following: * Convenient constructors for `binary_fan` and adjustments to its simp NF * Generalize the (co)kernel constructions in inclusions and projections of binary biproducts * Fixes the name of `kernel_fork.is_limit.of_ι` * Derives `preserves_limits_of_shape (discrete pempty) G` from the preservation of just *the* terminal morphism * Preserving zero morphisms implies preserving terminal morphisms * Isomorphisms from any fork to an application of `fork.of_ι` Co-authored-by: Markus Himmel <markus@himmel-villmar.de>