mathlib documentation

category_theory.limits.shapes.constructions.over.products

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.)