mathlib documentation

topology.sheaves.limits

Presheaves in C have limits and colimits when C does.

source
@[instance]
def Top.category_theory.limits.has_limits {C : Type u} [category_theory.category C] [category_theory.limits.has_limits C] (X : Top) :
category_theory.limits.has_limits (Top.presheaf C X)

source
@[instance]
def Top.category_theory.limits.has_colimits {C : Type u} [category_theory.category C] [category_theory.limits.has_colimits C] (X : Top) :
category_theory.limits.has_colimits (Top.presheaf C X)