When developing in Coq with the Universe Polymorphism flag on, the standard library introduces unwelcome universe constraints because it is universe monomorphic.
Is there an alternative standard library that is universe polymorphic? If not, are you aware of any plan to make the Coq standard library polymorphic?
Sadly, at the moment, there are no standard-ish libraries using universe polymorphism. A similar question arose some time ago and the Coq Zulip, and it seems multiple people from multiple projects which all reimplement some sort of universe polymorphic would be interested in such a universe polymorphic standard library, but this has not materialized into an actual library (yet).
I do not think there are any plans to turn the standard library polymorphic, at least not in the short term. Currently, universe-polymorphism in Coq is costly, and so making the standard library universe-polymorphic would degrade the performances of any development building on it, which in the Coq ecosystem is a red flag. But anyway as far as I understand the core developers want to move away from a single standard library packaged with Coq, and instead rely on possibly multiple ones with different choices as part of the Coq Platform. This way, users can choose the design decisions they prefer, typically monomorphic vs polymorphic universes.
So currently I would guess that the best thing is to take inspiration from or rely on the libraries out there that have significant polymorphic chunks. As far as I understand, this is the case of coq-ext-lib and Equations, MetaCoq also has a fair amount of universe polymorphic constructions available.
