α : Type u
β : Type v
γ : Type w
f : α → β
s : WSeq α
⊢ join (map (ret ∘ f) s) ~ʷ map f s
α : Type u
β : Type v
γ : Type w
f : α → β
s : WSeq α
⊢ bind s (ret ∘ f) ~ʷ map f s
dsimp [bind]
α : Type u
β : Type v
γ : Type w
f : α → β
s : WSeq α
⊢ join (map ret (map f s)) ~ʷ map f s
α : Type u
β : Type v
γ : Type w
f : α → β
s : WSeq α
⊢ join (map (ret ∘ f) s) ~ʷ map f s
rw [map_comp]
no goals
α : Type u
β : Type v
γ : Type w
f : α → β
s : WSeq α
⊢ join (map ret (map f s)) ~ʷ map f s
apply join_map_ret