Functoriality of multiset.
@[instance]
Equations
- multiset.functor = {map := multiset.map, map_const := λ (α β : Type u_1), multiset.map ∘ function.const β}
@[simp]
theorem
multiset.fmap_def
{α' β' : Type u_1}
{s : multiset α'}
(f : α' → β') :
f <$> s = multiset.map f s
@[instance]
Equations
def
multiset.traverse
{F : Type u → Type u}
[applicative F]
[is_comm_applicative F]
{α' β' : Type u} :
Equations
@[instance]
Equations
@[simp]
theorem
multiset.lift_beta
{α : 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}
(h : α → β) :
functor.map h ∘ coe = coe ∘ functor.map h
theorem
multiset.comp_traverse
{G H : Type u_1 → Type u_1}
[applicative G]
[applicative H]
[is_comm_applicative G]
[is_comm_applicative H]
{α β γ : 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]
[is_comm_applicative G]
{α β γ : 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]
[is_comm_applicative G]
{α β γ : Type u_1}
(g : α → β)
(h : β → G γ)
(x : multiset α) :
multiset.traverse h (multiset.map g x) = multiset.traverse (h ∘ g) x
theorem
multiset.naturality
{G H : Type u_1 → Type u_1}
[applicative G]
[applicative H]
[is_comm_applicative G]
[is_comm_applicative H]
(eta : applicative_transformation G H)
{α β : Type u_1}
(f : α → G β)
(x : multiset α) :
⇑eta (multiset.traverse f x) = multiset.traverse (⇑eta ∘ f) x