instLawfulBitraversableBicomplOfLawfulTraversable

Mathlib.Control.Bitraversable.Instances

URI: https://scilib.ai/kg/mathlib#instLawfulBitraversableBicomplOfLawfulTraversable

Lean4

instance [LawfulTraversable F] [LawfulTraversable G] [LawfulBitraversable t] : LawfulBitraversable (bicompl t F G) :=
  by
  constructor <;> intros <;>
    simp [bitraverse, Bicompl.bitraverse, bimap, traverse_id, bitraverse_id_id, comp_bitraverse, functor_norm]
  · simp [traverse_eq_map_id', bitraverse_eq_bimap_id]
  · dsimp only [bicompl]
    simp [binaturality, naturality_pf]

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

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

Разделы

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

Аффилиация

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