instMonadNormalExprMonoidalM

Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Monoidal.instMonadNormalExprMonoidalM

Lean4

instance : MonadNormalExpr MonoidalM
    where
  whiskerRightM η
    h := do
    return .whisker (← MonadMor₂.whiskerRightM η.e (.of h)) η h
  hConsM η
    θ := do
    return .cons (← MonadMor₂.horizontalCompM η.e θ.e) η θ
  whiskerLeftM f
    η := do
    return .whisker (← MonadMor₂.whiskerLeftM (.of f) η.e) f η
  nilM
    α := do
    return .nil (← MonadMor₂.homM α) α
  consM α η
    ηs := do
    return .cons (← MonadMor₂.comp₂M (← MonadMor₂.homM α) (← MonadMor₂.comp₂M η.e ηs.e)) α η ηs

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

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

Разделы

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

Аффилиация

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