Questions tagged [universe-polymorphism]
Universe polymorphism is the ability for definitions to be implicitly duplicated at different universe levels, with the types they contain. (from nLab).
12
questions
2
votes
1
answer
187
views
Lean 4: How can I specify that out of two universe variables, one is larger than the other?
Before Mathlib 4 was finished, I decided to implement my own ordinals, but this was as I was learning Lean 4, so my Ordinal type had type Type 1 instead of the ...
- 411
3
votes
2
answers
222
views
Universe inconsistency errors when using ZF model in Coq
I am trying to use a formal logic system I recently implemented in Coq to study ZF set theory. In order to do this, I need to define a type representing the domain in question, and then prove that ...
- 195
5
votes
1
answer
195
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
3
votes
0
answers
102
views
Using crude but effective stratification & cong to implement transitivity of `=`
Suppose I have
cong : {A B : Type} (f : A -> B) (p : a = b) : f a = f b
coe : (A : I -> Type) -> A 0 -> A 1
It is ...
- 6,306
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
377
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
8
votes
4
answers
246
views
What's the difference between a universe level and a natural number?
It seems that universe levels are just a type generated by a zero constant and a successor constructor (like in Agda), so why don't we adapt natural numbers as universe levels?
In Lean, it is also ...
- 6,306
15
votes
2
answers
417
views
In Agda, why is universe polymorphism explicit?
I've noticed that the process of coding a definition in Agda that is universe polymorphic usually requires little thought in how the Level parameters are specified. ...
- 361
13
votes
1
answer
429
views
Why did Agda give up cumulative universes?
In Ulf Norell's PhD thesis, which is considered the standard reference of the Agda 2 language, the universes are cumulative, say, Set i is not just an instance of <...
- 6,306
16
votes
1
answer
400
views
What happened to Conor McBride's universe polymorphism proposal?
Conor proposed a seemingly promising way towards universe polymorphism: https://mazzo.li/epilogue/index.html%3Fp=857&cpage=1.html IMHO, the idea behind this proposal is:
You build things starting ...
- 6,306