PR #4608: feat(category_theory/sites): sheaves on a groth...

Stream: triage

[Random Issue Bot]

Today I chose PR 4608 for discussion!

feat(category_theory/sites): sheaves on a grothendieck topology
Created by @Bhavik Mehta (@b-mehta) on 2020-10-13
Labels: awaiting-review

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

[Bhavik Mehta]

This is a big PR, but it's had a couple of comments and improvements by Johan and it passes all the linters, any more reviews on this appreciated

[Bhavik Mehta]

I'll ping the same people who Johan pinged on the PR before this: @Adam Topaz @Reid Barton @Kenny Lau @Kevin Buzzard @Markus Himmel if you'd like to review!

[Eric Wieser]

@Bhavik Mehta, none of those are real pings because they don't have the ** which zulip inserts automatically and it looks like you removed

[Bhavik Mehta]

Oops - I copied it from Johan's message so zulip didn't add it, thanks for letting me know!

[Bhavik Mehta]

@Adam Topaz @Reid Barton @Kenny Lau @Kevin Buzzard @Markus Himmel

[Kevin Buzzard]

Sorry I still didn't get to this -- it is literally at the top of my list of PR's to look at now but I spent all day interviewing. I will definitely look at it within the next few days.