All Questions
Tagged with universe-polymorphism universe
5
questions
5
votes
1
answer
196
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
108
views
Universe polymorphism and modules in Coq
The following code (without universe polymorphism) is accepted by Coq (8.16.0) :
...
- 175
7
votes
1
answer
378
views
Cardinality of Type in a given universe
I'm trying to determine the cardinality of Type u in Lean 3. So far I've been able to prove two inequalities:
...
- 173
11
votes
1
answer
243
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
8
votes
1
answer
228
views
Is there any universe polymorphic version of univalence?
People would say in univalent type theory, anything you defined for types should respect equivalence since univalence told you equivalence equivalent to equality. But that's not correct. Only ...
- 680