topos icon indicating copy to clipboard operation
topos copied to clipboard

Published 20 hours ago • verified publisher icon b-mehta

Kleisli categories

Open Vtec234 opened this issue 4 years ago • 0 comments

This is a roadmap for facts about Kleisli categories, which we should promptly send off to mathlib after proving.

  • [x] Kleisli category
  • [x] Kleisli adjunction
  • [ ] Category Adj(T) of adjunctions inducing the monad T
  • [ ] That the Kleisli adjunction and the Eilenberg-Moore adjunction (already in mathlib) are respectively initial and terminal in Adj(T) (5.2.12 here)

Vtec234 avatar Mar 12 '20 14:03 Vtec234