toLax

Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Pseudofunctor.toLax

Lean4

/-- The Lax functor associated with a pseudofunctor. -/
@[simps]
def toLax : LaxFunctor B C where
  toPrelaxFunctor := F.toPrelaxFunctor
  mapId := fun a => (F.mapId a).inv
  mapComp := fun f g => (F.mapComp f g).inv
  map₂_leftUnitor
    f := by
    rw [← F.map₂Iso_inv, eq_inv_comp, comp_inv_eq]
    simp
  map₂_rightUnitor
    f := by
    rw [← F.map₂Iso_inv, eq_inv_comp, comp_inv_eq]
    simp

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

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

Разделы

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

Аффилиация

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