English
The multiset construction forms a lawful monad with respect to the given applicative structure, i.e., it satisfies the monad laws (associativity of bind, left/right identity with pure, and compatibility with map).
Русский
Мультсет образует законную монаду относительно данного аппликативного устройства: выполняются все монады: ассоциативность связывания, левые и правые тождества с чистым и совместимость с отображением.
LaTeX
$$$\\text{LawfulMonad}({\\text{Multiset}})$$$
Lean4
instance : LawfulMonad Multiset :=
LawfulMonad.mk' (bind_pure_comp := fun _ _ ↦ by simp only [pure_def, bind_def, bind_singleton, fmap_def]) (id_map :=
fun _ ↦ by simp only [fmap_def, id_eq, map_id']) (pure_bind := fun _ _ ↦ by
simp only [pure_def, bind_def, singleton_bind]) (bind_assoc := @bind_assoc)
