English
The free magma construction carries a LawfulMonad structure, i.e., it satisfies the standard monad laws (pure, bind) and the LawfulMonad axioms (pure_bind, bind_assoc, id_map).
Русский
Свободная магма наделена структурой законного монады: выполняются стандартные законы монады (pure, bind) и оси закона LawfulMonad (чисто-связь, ассоциативность связывания, отображение единицы).
LaTeX
$$$$\text{FreeMagma is a LawfulMonad: pure_bind, bind_assoc, id_map hold. }$$$$
Lean4
@[to_additive]
instance instLawfulMonad : LawfulMonad FreeMagma.{u} :=
LawfulMonad.mk' (pure_bind := fun _ _ ↦ rfl) (bind_assoc := fun x f g ↦
FreeMagma.recOnPure x (fun _ ↦ rfl) fun x y ih1 ih2 ↦ by rw [mul_bind, mul_bind, mul_bind, ih1, ih2]) (id_map :=
fun x ↦ FreeMagma.recOnPure x (fun _ ↦ rfl) fun x y ih1 ih2 ↦ by rw [map_mul', ih1, ih2])
