Functoriality of Multiset.

instance Multiset.functor : Functor Multiset

Equations

• Multiset.functor = { map := @Multiset.map, mapConst := fun {α β : Type u_1} => Multiset.map ∘ Function.const β }

@[simp]

theorem Multiset.fmap_def {α' : Type u_1} {β' : Type u_1} {s : Multiset α'} (f : α' → β') : f <$> s = Multiset.map f s

instance Multiset.instLawfulFunctorMultisetFunctor : LawfulFunctor Multiset

Equations

• Multiset.instLawfulFunctorMultisetFunctor = ⋯

def Multiset.traverse {F : Type u → Type u} [Applicative F] [CommApplicative F] {α' : Type u} {β' : Type u} (f : α' → F β') : Multiset α' → F (Multiset β')

Map each element of a Multiset to an action, evaluate these actions in order, and collect the results.

Equations

• Multiset.traverse f = Quotient.lift (Functor.map Coe.coe ∘ traverse f) ⋯

instance Multiset.instMonadMultiset : Monad Multiset

Equations

• Multiset.instMonadMultiset = let __src := Multiset.functor; Monad.mk

@[simp]

theorem Multiset.pure_def {α : Type u_1} : pure = singleton

@[simp]

theorem Multiset.bind_def {α : Type u_1} {β : Type u_1} : (fun (x : Multiset α) (x_1 : α → Multiset β) => x >>= x_1) = Multiset.bind

instance Multiset.instLawfulMonadMultisetInstMonadMultiset : LawfulMonad Multiset

Equations

• Multiset.instLawfulMonadMultisetInstMonadMultiset = ⋯

@[simp]

theorem Multiset.lift_coe {α : Type u_1} {β : Type u_2} (x : List α) (f : List α → β) (h : ∀ (a b : List α), a ≈ b → f a = f b) : Quotient.lift f h ↑x = f x

@[simp]

theorem Multiset.map_comp_coe {α : Type u_1} {β : Type u_1} (h : α → β) : Functor.map h ∘ Coe.coe = Coe.coe ∘ Functor.map h

theorem Multiset.id_traverse {α : Type u_1} (x : Multiset α) : Multiset.traverse pure x = x

theorem Multiset.comp_traverse {G : Type u_1 → Type u_1} {H : Type u_1 → Type u_1} [Applicative G] [Applicative H] [CommApplicative G] [CommApplicative H] {α : Type u_1} {β : Type u_1} {γ : Type u_1} (g : α → G β) (h : β → H γ) (x : Multiset α) : Multiset.traverse (Functor.Comp.mk ∘ Functor.map h ∘ g) x = Functor.Comp.mk (Multiset.traverse h <$> Multiset.traverse g x)

theorem Multiset.map_traverse {G : Type u_1 → Type u_1} [Applicative G] [CommApplicative G] {α : Type u_1} {β : Type u_1} {γ : Type u_1} (g : α → G β) (h : β → γ) (x : Multiset α) : Functor.map h <$> Multiset.traverse g x = Multiset.traverse (Functor.map h ∘ g) x

theorem Multiset.traverse_map {G : Type u_1 → Type u_1} [Applicative G] [CommApplicative G] {α : Type u_1} {β : Type u_1} {γ : Type u_1} (g : α → β) (h : β → G γ) (x : Multiset α) : Multiset.traverse h (Multiset.map g x) = Multiset.traverse (h ∘ g) x

theorem Multiset.naturality {G : Type u_1 → Type u_1} {H : Type u_1 → Type u_1} [Applicative G] [Applicative H] [CommApplicative G] [CommApplicative H] (eta : ApplicativeTransformation G H) {α : Type u_1} {β : Type u_1} (f : α → G β) (x : Multiset α) : (fun {α : Type u_1} => eta.app α) (Multiset.traverse f x) = Multiset.traverse ((fun {α : Type u_1} => eta.app α) ∘ f) x