instLawfulBitraversableBicomprOfLawfulTraversable

Mathlib.Control.Bitraversable.Instances

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

Lean4

instance [LawfulTraversable F] [LawfulBitraversable t] : LawfulBitraversable (bicompr F t) :=
  by
  constructor <;> intros <;> simp [bitraverse, Bicompr.bitraverse, bitraverse_id_id, functor_norm]
  · simp only [bitraverse_eq_bimap_id', traverse_eq_map_id', Function.comp_apply]; rfl
  · dsimp only [bicompr]
    simp [naturality, binaturality']

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

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

Разделы

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

Аффилиация

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