Documentation

Mathlib.CategoryTheory.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

@[reducible, inline]

Define the equalizing object

Equations
  • One or more equations did not get rendered due to their size.
Instances For