---

Step * of Lemma bag-cat-monad_wf

No Annotations
bag-cat-monad() ∈ Monad(TypeCat)
BY
{ ((Assert TypeCat ∈ SmallCategory' BY
          Auto)
   THEN (Assert functor(ob(x) = bag(x);
                        arrow(x,y,f) = λz.bag-map(f;z)) ∈ Functor(TypeCat;TypeCat) BY
               ((Auto THEN All (RepUR ``type-cat``)) THEN Auto))
   THEN (Assert x |→ λz.{z} ∈ nat-trans(TypeCat;TypeCat;1;functor(ob(x) = bag(x);
                                                                  arrow(x,y,f) = λz.bag-map(f;z))) BY
               (Auto THEN All (RepUR ``type-cat id_functor compose``) THEN Auto))) }

1
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)

---

Latex:

---

Latex:
No  Annotations
bag-cat-monad()  \mmember{}  Monad(TypeCat)


By

---

Latex:
((Assert  TypeCat  \mmember{}  SmallCategory'  BY
                Auto)
  THEN  (Assert  functor(ob(x)  =  bag(x);
                                            arrow(x,y,f)  =  \mlambda{}z.bag-map(f;z))  \mmember{}  Functor(TypeCat;TypeCat)  BY
                          ((Auto  THEN  All  (RepUR  ``type-cat``))  THEN  Auto))
  THEN  (Assert  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)))  BY
                          (Auto  THEN  All  (RepUR  ``type-cat  id\_functor  compose``)  THEN  Auto)))

---

Home Index