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).

Filter by
Sorted by
Tagged with
2 votes
0 answers
62 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 ...
  • 4,992
3 votes
1 answer
77 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
202 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: ...
11 votes
1 answer
192 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,061
8 votes
1 answer
166 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 ...
7 votes
4 answers
179 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 ...
  • 4,992
12 votes
2 answers
262 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. ...
11 votes
1 answer
296 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 <...
  • 4,992
14 votes
1 answer
298 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 ...
  • 4,992