comp

Mathlib.CategoryTheory.Enriched.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.EnrichedFunctor.comp

Lean4

/-- Composition of enriched functors. -/
@[simps]
def comp {C : Type u₁} {D : Type u₂} {E : Type u₃} [EnrichedCategory V C] [EnrichedCategory V D] [EnrichedCategory V E]
    (F : EnrichedFunctor V C D) (G : EnrichedFunctor V D E) : EnrichedFunctor V C E
    where
  obj X := G.obj (F.obj X)
  map _ _ := F.map _ _ ≫ G.map _ _

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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