Verify upper shriek functors give pseudo functor

This is really not bad at all, but of course it looks kinda bad because
we try to really give the details...