Commit 2020-04-23 01:10 4d94de48View on Github →
feat(category_theory): wide pullbacks and limits in the over category (#2461)
This PR introduces wide pullbacks.
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.