All Questions
3
questions
5
votes
1
answer
200
views
Universe polymorphism and Coq standard library
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 ...
- 75
4
votes
1
answer
109
views
Universe polymorphism and modules in Coq
The following code (without universe polymorphism) is accepted by Coq (8.16.0) :
...
- 175
11
votes
1
answer
244
views
How much duplication does universe polymorphism actually save us?
From my rough impression, in (formalizing) everyday mathematics we almost never use universe polymorphism in a way that stretches the proof-theoretic strength. It merely saves us some duplication.
My ...
- 4,025