mathlib documentation

category_theory.limits.constructions.over.default

Limits in the over category #

Declare instances for limits in the over category: If C has finite wide pullbacks, over B has finite limits, and if C has arbitrary wide pullbacks then over B has limits.