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: generalize universe

A functor that preserves pullbacks and binary products also presrves equalizers.

Equations

A functor that preserves pushouts and binary coproducts also presrves coequalizers.

Equations