mathlib documentation

category_theory.limits.shapes.normal_mono.equalizers

Normal mono categories with finite products and kernels have all equalizers. #

This, and the dual result, are used in the development of abelian categories.