Kleisli categories - Githubissues

b-mehta / topos

Topos theory in lean

55 stars 2 forks source link

Kleisli categories #32

Open Vtec234 opened 4 years ago

Vtec234 commented 4 years ago

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)