English
FreeSemigroup is a LawfulTraversable; its lawful traversable structure extends the lawful monad structure to traversals.
Русский
FreeSemigroup является LawfulTraversable; его законная структураTraversable расширяет законную монадную структуру на обходы.
LaTeX
$$$\text{LawfulTraversable}(\text{FreeSemigroup})$$$
Lean4
@[to_additive]
instance : LawfulTraversable FreeSemigroup.{u} :=
{
instLawfulMonad with
id_traverse := fun x ↦
FreeSemigroup.recOnMul x (fun _ ↦ rfl) fun x y ih1 ih2 ↦ by
rw [traverse_mul, ih1, ih2, seq_pure, map_pure, map_pure]
comp_traverse := fun f g x ↦
recOnPure x (fun x ↦ by simp only [traverse_pure, functor_norm, Function.comp_def]) fun x y ih1 ih2 ↦
by
rw [traverse_mul, ih1, ih2, traverse_mul, Functor.Comp.map_mk]
simp only [Function.comp_def, functor_norm, traverse_mul]
naturality := fun η α β f x ↦
recOnPure x (fun x ↦ by simp only [traverse_pure, functor_norm, Function.comp])
(fun x y ih1 ih2 ↦ by simp only [traverse_mul, functor_norm, ih1, ih2])
traverse_eq_map_id := fun f x ↦
FreeSemigroup.recOnMul x (fun _ ↦ rfl) fun x y ih1 ih2 ↦ by
rw [traverse_mul, ih1, ih2, map_mul', map_pure, seq_pure, map_pure] }
