ofQuivHom

Mathlib.CategoryTheory.Category.Quiv

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Prefunctor.ofQuivHom

Lean4

/-- Arrows in `Quiv` define prefunctors. -/
def ofQuivHom {C D : Quiv} (F : C ⟶ D) : C ⥤q D :=
  F

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

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

Разделы

Аффилиация

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