inst

Mathlib.CategoryTheory.Bicategory.Adjunction.Adj

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Bicategory.Adj.inst

Lean4

@[simps! whiskerRight_τr whiskerRight_τl whiskerLeft_τr whiskerLeft_τl associator_hom_τr associator_inv_τr
      associator_hom_τl associator_inv_τl leftUnitor_hom_τr leftUnitor_inv_τr leftUnitor_hom_τl leftUnitor_inv_τl
      rightUnitor_hom_τr rightUnitor_inv_τr rightUnitor_hom_τl rightUnitor_inv_τl]
instance : Bicategory (Adj B) where
  whiskerLeft := Bicategory.whiskerLeft
  whiskerRight := Bicategory.whiskerRight
  associator := Bicategory.associator
  leftUnitor := Bicategory.leftUnitor
  rightUnitor := Bicategory.rightUnitor

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

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

Разделы

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

Аффилиация

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