---

Step * of Lemma bag-monad_wf

BagMonad ∈ Monad
BY
{ ProveWfLemma }

1
1. T : Type
2. S : Type
3. x : T
4. f : T ⟶ ((λT.bag(T)) S)@i
⊢ ((λba,f. ⋃x∈ba.f x) ((λx.{x}) x) f) = (f x) ∈ ((λT.bag(T)) S)

2
1. T : Type
2. m : (λT.bag(T)) T
⊢ ((λba,f. ⋃x∈ba.f x) m (λx.{x})) = m ∈ ((λT.bag(T)) T)

3
1. T : Type
2. S : Type
3. U : Type
4. m : (λT.bag(T)) T
5. f : T ⟶ ((λT.bag(T)) S)
6. g : S ⟶ ((λT.bag(T)) U)
⊢ ((λba,f. ⋃x∈ba.f x) ((λba,f. ⋃x∈ba.f x) m f) g) = ((λba,f. ⋃x∈ba.f x) m (λx.((λba,f. ⋃x∈ba.f x) (f x) g))) ∈ ((λT.bag(\000CT)) U)

---

Latex:

---

Latex:
BagMonad  \mmember{}  Monad


By

---

Latex:
ProveWfLemma

---

Home Index