Kleisli categories - Githubissues

b-mehta / topos

Topos theory in lean

56 stars 2 forks source link

Kleisli categories #31

Closed Vtec234 closed 4 years ago

Vtec234 commented 4 years ago

This PR is to track progress on adding facts about Kleisli categories. What we might (?) want to have before merging this PR:

[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)~

b-mehta commented 4 years ago

I'd be happy to merge with the first two, and leave the other two for further PRs. Also these all should probably go to mathlib

Vtec234 commented 4 years ago

Sure, then I'll put this roadmap in an issue. The adjunction is almost finished modulo the right triangle equality which involves heqs and which I can't think of a way to prove in a non-horrible way.

b-mehta commented 4 years ago

I'm reasonably happy to merge this if you are