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

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

Universe polymorphism and modules in Coq

The following code (without universe polymorphism) is accepted by Coq (8.16.0) : ...
  • 133
7 votes
1 answer

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

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

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

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

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

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

What happened to Conor McBride's universe polymorphism proposal?

Conor proposed a seemingly promising way towards universe polymorphism: IMHO, the idea behind this proposal is: You build things starting ...
  • 4,992