# 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: May 18 2021 at 23:14 UTC