instLawfulTraversable — Mathlib

English

The type Tree is equipped with a LawfulTraversable instance, expressing compatibility of map and traverse with identity and composition laws.

Русский

Тип Tree имеет экземпляр LawfulTraversable, задающий совместимость отображения и перебора с законами идентичности и композиции.

LaTeX

$$$ \text{LawfulTraversable(Tree)} $$$

Lean4

instance : LawfulTraversable Tree where
  map_const := rfl
  id_map := id_map
  comp_map := comp_map
  id_traverse t := traverse_pure t
  comp_traverse := comp_traverse
  traverse_eq_map_id := traverse_eq_map_id
  naturality η := naturality η

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