naturality

Mathlib.Control.Traversable.Instances

URI: https://scilib.ai/kg/mathlib#Option.naturality

Lean4

theorem naturality [LawfulApplicative F] {α β} (f : α → F β) (x : Option α) :
    η (Option.traverse f x) = Option.traverse (@η _ ∘ f) x := by
  rcases x with - | x <;> simp! [*, functor_norm, Option.traverse]

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

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

Разделы

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

Аффилиация

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