Zulip Chat Archive
Stream: triage
Topic: PR #4885: feat(category_theory/adjunction): general adjoi...
Random Issue Bot (Nov 26 2020 at 14:20):
Today I chose PR 4885 for discussion!
feat(category_theory/adjunction): general adjoint functor theorem
Created by @Bhavik Mehta (@b-mehta) on 2020-11-03
Labels: maybe-later, needs-documentation
Is this PR still relevant? Any recent updates? Anyone making progress?
Bhavik Mehta (Nov 26 2020 at 17:38):
No recent updates on this, I don't have any particular need for the results here and I have other more pressing things. I'd like to get it in mathlib eventually since it's cool and should be in category theory in mathlib, but I just don't have the time for it right now
Random Issue Bot (Mar 08 2021 at 14:21):
Today I chose PR 4885 for discussion!
feat(category_theory/adjunction): general adjoint functor theorem
Created by @Bhavik Mehta (@b-mehta) on 2020-11-03
Labels: maybe-later, needs-documentation
Is this PR still relevant? Any recent updates? Anyone making progress?
Bhavik Mehta (Mar 08 2021 at 14:44):
As before
Last updated: Dec 20 2023 at 11:08 UTC