Theorems · Inductive type · category theory

CategoryTheory.Limits.HasLimitsOfShape

(J : Type u₁) → [CategoryTheory.Category.{v₁, u₁} J] → (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop

C has limits of shape J if there exists a limit for every functor F : J ⥤ C.

Defined in

Mathlib.CategoryTheory.Limits.HasLimits

Cited by

223 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.Category