naturality

Mathlib.Control.Traversable.Instances

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

Lean4

protected theorem naturality {α β} (f : α → F β) (x : σ ⊕ α) : η (Sum.traverse f x) = Sum.traverse (@η _ ∘ f) x := by
  cases x <;> simp! [Sum.traverse, functor_norm]

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

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

Разделы

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

Аффилиация

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