@andrejbauer asks "what's the solution?" To use as few packages as possible. I spent a long time, some months ago, trying to find a fix for cleverref. For my collaborator it worked, because they had an old version of LaTeX, but for me it didn't. It was so frustrating. I subscribe to @jonmsterling 's position of using Spartan LaTeX. In TypeTopology we use both Spartan MLTT, and even more Spartan Agda, deliberately.