toOplax

Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

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

Lean4

/-- The oplax functor associated with a pseudofunctor. -/
@[simps]
def toOplax : OplaxFunctor B C where
  toPrelaxFunctor := F.toPrelaxFunctor
  mapId := fun a => (F.mapId a).hom
  mapComp := fun f g => (F.mapComp f g).hom

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

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

Разделы

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

Аффилиация

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