toStrictlyUnitaryLaxFunctor

Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

URI: https://scilib.ai/kg/mathlib#CategoryTheory.StrictlyUnitaryPseudofunctor.toStrictlyUnitaryLaxFunctor

Lean4

/-- By forgetting the inverse to `mapComp`, a `StrictlyUnitaryPseudofunctor`
is a `StrictlyUnitaryLaxFunctor`. -/
def toStrictlyUnitaryLaxFunctor (F : StrictlyUnitaryPseudofunctor B C) : StrictlyUnitaryLaxFunctor B C
    where
  __ := F.toPseudofunctor.toLax
  map_id x := by simp [F.map_id]
  mapId_eq_eqToHom x := by simp [F.mapId_eq_eqToIso]

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

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

Разделы

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

Аффилиация

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