toLaxMonoidal

Mathlib.CategoryTheory.Monoidal.Functor

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.CoreMonoidal.toLaxMonoidal

Lean4

/-- The lax monoidal functor structure induced by a `Functor.CoreMonoidal` structure. -/
@[simps -isSimp]
def toLaxMonoidal : F.LaxMonoidal where
  ε := h.εIso.hom
  μ X Y := (h.μIso X Y).hom
  left_unitality := h.left_unitality
  right_unitality := h.right_unitality

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

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

Разделы

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

Аффилиация

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