categoryObjects

Mathlib.CategoryTheory.Category.Cat.Limit

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Cat.HasLimits.categoryObjects

Lean4

instance categoryObjects {F : J ⥤ Cat.{u, u}} {j} : SmallCategory ((F ⋙ Cat.objects.{u, u}).obj j) :=
  (F.obj j).str

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru