ιPaths

Mathlib.CategoryTheory.Localization.Construction

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Localization.Construction.ιPaths

Lean4

/-- The object in the path category of `LocQuiver W` attached to an object in
the category `C` -/
def ιPaths (X : C) : Paths (LocQuiver W) :=
  ⟨X⟩

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

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

Разделы

Аффилиация

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