instEnrichedCategorySSet

Mathlib.AlgebraicTopology.SimplicialCategory.SimplicialObject

URI: https://scilib.ai/kg/mathlib#CategoryTheory.SimplicialObject.instEnrichedCategorySSet

Lean4

noncomputable instance : EnrichedCategory SSet.{v} (SimplicialObject D) :=
  inferInstanceAs (EnrichedCategory (_ ⥤ Type v) (_ ⥤ D))

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

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

Разделы

Аффилиация

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