Companion to stdpp!368 (merged).
- updates the code to use the fixpoint versions of
- Uses some explicit universe annotations to reduce the overall number of universes (very slightly). These universes are given explicit names and documented.
I think 2 is an overall improvement, but I do not think it is strictly necessary.