bicategory

Mathlib.CategoryTheory.Enriched.EnrichedCat

URI: https://scilib.ai/kg/mathlib#CategoryTheory.EnrichedCat.bicategory

Lean4

/-- The bicategory structure on `EnrichedCat V` for a monoidal category `V`. -/
instance bicategory : Bicategory (EnrichedCat.{w, v, u} V)
    where
  Hom C D := EnrichedFunctor V C D
  id C := EnrichedFunctor.id V C
  comp F G := EnrichedFunctor.comp V F G
  whiskerLeft F G H := whiskerLeft F
  whiskerRight := whiskerRight
  associator := associator
  leftUnitor := leftUnitor
  rightUnitor := rightUnitor
  comp_whiskerRight := comp_whiskerRight
  whisker_exchange := whisker_exchange

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

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

Разделы

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

Аффилиация

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