6:58 AM
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)