Zulip Chat Archive

Stream: triage

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


view this post on Zulip Random Issue Bot (Nov 13 2020 at 14:17):

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?

view this post on Zulip Bhavik Mehta (Nov 13 2020 at 15:16):

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

view this post on Zulip Bhavik Mehta (Nov 13 2020 at 15:18):

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!

view this post on Zulip Eric Wieser (Nov 13 2020 at 15:28):

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

view this post on Zulip Bhavik Mehta (Nov 13 2020 at 15:31):

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

view this post on Zulip Bhavik Mehta (Nov 13 2020 at 15:31):

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

view this post on Zulip Kevin Buzzard (Nov 13 2020 at 17:36):

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.


Last updated: May 09 2021 at 16:20 UTC