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).
11
questions
3
votes
2
answers
198
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
169
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
84
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 ...
- 5,877
3
votes
1
answer
92
views
Universe polymorphism and modules in Coq
The following code (without universe polymorphism) is accepted by Coq (8.16.0) :
...
- 133
7
votes
1
answer
278
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
227
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 ...
- 3,688
8
votes
1
answer
212
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 ...
- 660
8
votes
4
answers
227
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 ...
- 5,877
14
votes
2
answers
349
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. ...
- 351
13
votes
1
answer
366
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 <...
- 5,877
15
votes
1
answer
368
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 ...
- 5,877