mathlib3

4d94de48 - feat(category_theory): wide pullbacks and limits in the over category (#2461)

feat(category_theory): wide pullbacks and limits in the over category (#2461) This PR introduces [wide pullbacks](https://ncatlab.org/nlab/show/wide+pullback). Ordinary pullbacks are then defined as a special case of wide pullbacks, which simplifies some of the definitions and proofs there. Finally we show that the existence of wide pullbacks in `C` gives products in the slice `C/B`, and in fact gives all limits. Co-authored-by: Keeley Hoek <keeley@hoek.io>