Zulip Chat Archive

Stream: triage

Topic: PR #4885: feat(category_theory/adjunction): general adjoi...


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Bhavik Mehta (Mar 08 2021 at 14:44):

As before


Last updated: May 18 2021 at 23:14 UTC