instMonadNormalExprBicategoryM

Mathlib.Tactic.CategoryTheory.Bicategory.Normalize

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Bicategory.instMonadNormalExprBicategoryM

Lean4

instance : MonadNormalExpr BicategoryM
    where
  whiskerRightM η
    h := do
    return .whisker (← MonadMor₂.whiskerRightM η.e (.of h)) η h
  hConsM _
    _ := do
    throwError"not implemented"
  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