mathlib3 documentation

category_theory.limits.constructions.equalizers

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.

Equations

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

Equations