equiv

Mathlib.Control.Monad.Writer

URI: https://scilib.ai/kg/mathlib#WriterT.equiv

Lean4

/-- reduce the equivalence between two writer monads to the equivalence between
their underlying monad -/
def equiv {m₁ : Type u₀ → Type v₀} {m₂ : Type u₁ → Type v₁} {α₁ ω₁ : Type u₀} {α₂ ω₂ : Type u₁}
    (F : (m₁ (α₁ × ω₁)) ≃ (m₂ (α₂ × ω₂))) : WriterT ω₁ m₁ α₁ ≃ WriterT ω₂ m₂ α₂
    where
  toFun (f : m₁ _) := WriterT.mk <| F f
  invFun (f : m₂ _) := WriterT.mk <| F.symm f
  left_inv (f : m₁ _) := congr_arg WriterT.mk <| F.left_inv f
  right_inv (f : m₂ _) := congr_arg WriterT.mk <| F.right_inv f

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

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

Разделы

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

Аффилиация

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