Documentation

Mathlib.CategoryTheory.Limits.Shapes.NormalMono.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.