Zulip Chat Archive
Stream: triage
Topic: PR #4930: feat(category_theory/closed): Exponential ideals
Random Issue Bot (Dec 31 2020 at 14:32):
Today I chose PR 4930 for discussion!
feat(category_theory/closed): Exponential ideals
Created by @Bhavik Mehta (@b-mehta) on 2020-11-07
Labels: WIP, merge-conflict, not-ready-to-merge
Is this PR still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Jan 14 2021 at 14:46):
Today I chose PR 4930 for discussion!
feat(category_theory/closed): Exponential ideals
Created by @Bhavik Mehta (@b-mehta) on 2020-11-07
Labels: WIP, not-ready-to-merge
Is this PR still relevant? Any recent updates? Anyone making progress?
Bhavik Mehta (Jan 16 2021 at 16:31):
Currently blocked on #5680 and maybe a couple of other things, but this is still on my radar
Random Issue Bot (Feb 20 2021 at 14:19):
Today I chose PR 4930 for discussion!
feat(category_theory/closed): Exponential ideals
Created by @Bhavik Mehta (@b-mehta) on 2020-11-07
Labels: WIP, not-ready-to-merge
Is this PR still relevant? Any recent updates? Anyone making progress?
Last updated: Dec 20 2023 at 11:08 UTC