mathlib documentation

category_theory.limits.shapes.constructions.over.default

source
@[instance]
def category_theory.over.has_finite_limits {C : Type u} [category_theory.category C] {B : C} [category_theory.limits.has_finite_wide_pullbacks C] :
category_theory.limits.has_finite_limits (category_theory.over B)

source
@[instance]
def category_theory.over.has_limits {C : Type u} [category_theory.category C] {B : C} [category_theory.limits.has_wide_pullbacks C] :
category_theory.limits.has_limits (category_theory.over B)