---

Step * of Lemma monad-unit_wf

∀[C:SmallCategory]. ∀[M:Monad(C)]. ∀[x:cat-ob(C)].  (monad-unit(M;x) ∈ cat-arrow(C) x M(x))
BY
{ (ProveWfLemma
   THEN D 2
   THEN DProds
   THEN D 3
   THEN RepUR ``monad-fun monad-functor`` 0
   THEN All (RepUR  ``id_functor``)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[C:SmallCategory].  \mforall{}[M:Monad(C)].  \mforall{}[x:cat-ob(C)].    (monad-unit(M;x)  \mmember{}  cat-arrow(C)  x  M(x))


By

---

Latex:
(ProveWfLemma
  THEN  D  2
  THEN  DProds
  THEN  D  3
  THEN  RepUR  ``monad-fun  monad-functor``  0
  THEN  All  (RepUR    ``id\_functor``)
  THEN  Auto)

---

Home Index