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

Stream: triage

[Random Issue Bot]

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]

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