Zulip Chat Archive

Stream: triage

Topic: PR #5282: feat(category_theory/sites): closed sieves


Random Issue Bot (Dec 27 2020 at 14:27):

Today I chose PR 5282 for discussion!

feat(category_theory/sites): closed sieves
Created by @Bhavik Mehta (@b-mehta) on 2020-12-08
Labels: WIP

Is this PR still relevant? Any recent updates? Anyone making progress?

Bhavik Mehta (Dec 27 2020 at 14:37):

Haven't really touched this in a little while, I'll come back to it at some point though since some of these results are helpful, I think there's no urgency for this at the moment


Last updated: Dec 20 2023 at 11:08 UTC