mathlib documentation


Products in the over category #

Shows that products in the over category can be derived from wide pullbacks in the base category. The main result is over_product_of_wide_pullback, which says that if C has J-indexed wide pullbacks, then over B has J-indexed products.

(Implementation) Given a product diagram in C/B, construct the corresponding wide pullback diagram in C.


Construct terminal object in the over category. This isn't an instance as it's not typically the way we want to define terminal objects. (For instance, this gives a terminal object which is different from the generic one given by over_product_of_wide_pullback above.)