mathlib3 documentation


Constructing equalizers from pullbacks and binary products. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.


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