---

Step * of Lemma monad-extend_wf

∀[C:SmallCategory]. ∀[M:Monad(C)]. ∀[x,y:cat-ob(C)]. ∀[f:cat-arrow(C) x M(y)].
  (monad-extend(C;M;x;y;f) ∈ cat-arrow(C) M(x) M(y))
BY
{ (Intros
   THEN Unhide
   THEN D 2
   THEN DProds
   THEN All Reduce
   THEN All (RepUR ``monad-extend monad-fun monad-functor monad-op``)
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Intros
  THEN  Unhide
  THEN  D  2
  THEN  DProds
  THEN  All  Reduce
  THEN  All  (RepUR  ``monad-extend  monad-fun  monad-functor  monad-op``)
  THEN  Auto)

---

Home Index