isLawfulTraversable

Mathlib.Control.Bitraversable.Instances

URI: https://scilib.ai/kg/mathlib#Bitraversable.isLawfulTraversable

Lean4

instance (priority := 10) isLawfulTraversable [LawfulBitraversable t] {α} : LawfulTraversable (t α) :=
  by
  constructor <;> intros <;> simp [traverse, comp_tsnd, functor_norm]
  · simp [tsnd_eq_snd_id, (· <$> ·)]
  · simp [tsnd, binaturality, Function.comp_def, functor_norm]

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

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

Разделы

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

Аффилиация

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