English
The FreeMagma construction is LawfulTraversable, i.e., traversing with respect to any Applicative commutes with composition in the prescribed way, satisfying the laws of traversable functors.
Русский
Свободная магма образует законноеTraversable, то есть обход с учётом Applicative согласуется с композицией и удовлетворяет законам обходного функтoра.
LaTeX
$$$$\text{FreeMagma is LawfulTraversable: id_traverse, comp_traverse, naturality, traverse_eq_map_id hold.}$$$$
Lean4
@[to_additive]
instance : LawfulTraversable FreeMagma.{u} :=
{
instLawfulMonad with
id_traverse := fun x ↦
FreeMagma.recOnPure 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 ↦
FreeMagma.recOnPure x (fun x ↦ by simp only [Function.comp_def, traverse_pure, functor_norm])
(fun x y ih1 ih2 ↦ by
rw [traverse_mul, ih1, ih2, traverse_mul]
simp [Functor.Comp.map_mk, Functor.map_map, Function.comp_def, Comp.seq_mk, seq_map_assoc, map_seq,
traverse_mul])
naturality := fun η α β f x ↦
FreeMagma.recOnPure x (fun x ↦ by simp only [traverse_pure, functor_norm, Function.comp_apply])
(fun x y ih1 ih2 ↦ by simp only [traverse_mul, functor_norm, ih1, ih2])
traverse_eq_map_id := fun f x ↦
FreeMagma.recOnPure x (fun _ ↦ rfl) fun x y ih1 ih2 ↦ by
rw [traverse_mul, ih1, ih2, map_mul', map_pure, seq_pure, map_pure] }
