@JonathanBeardsley You are good at math. FYI

The privilege you have doesn't undercut that.

@ClarkBarwick <3

^ (that came out far more sarcastically than I intended)

Hi Piotr, first of all I have to correct myself since i was being sloppy about sheaves vs hypersheaves. Instead of considering all sheaves on anima (on the usual site of open subsets of S) let me just fix a d and consider sheaves of d-truncated anima. Then we avoid all these issues and it's still enough to deduce cohomology statements.

Then the point is you can detect equivalences on stalks, so any time you hae a surjective map T --> S the pullback detects equivalences

Thus if T --> S is both proper and surjective, the pullback is conservative and adjointable and you have Beck-Chevally all the way up the Cech nerve so the discussion of descent in HA 4.7.5 gives what you want

(the business about sheaves vs hypersheaves is a bit annoying here, because only for hypersheaves is pullback along surjective maps conservative, but only for honest sheaves do you have proper base change... and we actually do end up applying this statement to an infinite product of copies of circles, where not every sheaf is a hypersheaf. But ok, we only need truncated sheaves)

@DustinClausen Thank you, that was super helpful. :)

@ReubenStern Yeah I mean, one thing I get excited about as a mathematician is, like spreading knowledge and connecting people with one another. And of course I don't mind being in the room when these people start talking to one another. =P