category

Mathlib.CategoryTheory.Enriched.Basic

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

Lean4

/-- Enriched functors form a category with the morphisms between functors `F` and `G` being
enriched natural transformations, i.e. natural transformations `F.forget ⟶ G.forget`. -/
@[simps]
instance category : Category (EnrichedFunctor V C D)
    where
  Hom F G := EnrichedNatTrans F G
  id F := ⟨𝟙 _⟩
  comp F G := ⟨F.out ≫ G.out⟩

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

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

Разделы

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

Аффилиация

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