bicategory

Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory

Lean4

/-- A bicategory structure on the oplax functors between bicategories. -/
@[simps!]
scoped instance bicategory : Bicategory (OplaxFunctor B C)
    where
  whiskerLeft {_ _ _} η _ _ Γ := whiskerLeft η Γ
  whiskerRight {_ _ _} _ _ Γ η := whiskerRight Γ η
  associator {_ _ _} _ := associator
  leftUnitor {_ _} := leftUnitor
  rightUnitor {_ _} := rightUnitor
  whisker_exchange {a b c f g h i} η
    θ := by
    ext
    exact whisker_exchange _ _

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

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

Разделы

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

Аффилиация

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