---

Step * 1 of Lemma bag-cat-monad_wf


1. TypeCat ∈ SmallCategory'
2. functor(ob(x) = bag(x);
           arrow(x,y,f) = λz.bag-map(f;z)) ∈ Functor(TypeCat;TypeCat)
3. x |→ λz.{z} ∈ nat-trans(TypeCat;TypeCat;1;functor(ob(x) = bag(x);
                                                     arrow(x,y,f) = λz.bag-map(f;z)))
⊢ bag-cat-monad() ∈ Monad(TypeCat)
BY
{ (Unfold `bag-cat-monad` 0
   THEN MemCD
   THEN Try (Trivial)
   THEN Try ((RepUR ``type-cat compose`` 0 THEN Try (Fold `bag-combine` 0) THEN Complete (Auto)))
   THEN (Auto THEN All (RepUR ``type-cat id_functor compose functor-comp``))
   THEN Auto) }

---

Latex:

---

Latex:

1.  TypeCat  \mmember{}  SmallCategory'
2.  functor(ob(x)  =  bag(x);
                      arrow(x,y,f)  =  \mlambda{}z.bag-map(f;z))  \mmember{}  Functor(TypeCat;TypeCat)
3.  x  |\mrightarrow{}  \mlambda{}z.\{z\}  \mmember{}  nat-trans(TypeCat;TypeCat;1;functor(ob(x)  =  bag(x);
                                                                                                          arrow(x,y,f)  =  \mlambda{}z.bag-map(f;z)))
\mvdash{}  bag-cat-monad()  \mmember{}  Monad(TypeCat)


By

---

Latex:
(Unfold  `bag-cat-monad`  0
  THEN  MemCD
  THEN  Try  (Trivial)
  THEN  Try  ((RepUR  ``type-cat  compose``  0  THEN  Try  (Fold  `bag-combine`  0)  THEN  Complete  (Auto)))
  THEN  (Auto  THEN  All  (RepUR  ``type-cat  id\_functor  compose  functor-comp``))
  THEN  Auto)

---

Home Index