# 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
Filter by
Sorted by
Tagged with
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 ...
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
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
92 views

### Universe polymorphism and modules in Coq

The following code (without universe polymorphism) is accepted by Coq (8.16.0) : ...
• 133
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
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
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
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
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. ...
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