Commit 2020-04-23 01:10 4d94de48

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.