mathlib documentation

category_theory.limits.constructions.equalizers

Constructing equalizers from pullbacks and binary products. #

If a category has pullbacks and binary products, then it has equalizers.

TODO: provide the dual result.