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