# mathlibdocumentation

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.

@[instance]
@[instance]