Step
*
of Lemma
monad-functor_wf
No Annotations
∀[C:SmallCategory]. ∀[M:Monad(C)].  (monad-functor(M) ∈ Functor(C;C))
BY
{ ProveWfLemma }
Latex:
Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[M:Monad(C)].    (monad-functor(M)  \mmember{}  Functor(C;C))
By
Latex:
ProveWfLemma
Home
Index