Skip to main content

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
1 answer

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 ...
Jozef Mikušinec's user avatar
3 votes
2 answers

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 ...
Circuit Craft's user avatar
5 votes
1 answer

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 ...
Jon's user avatar
  • 75
3 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 ...
ice1000's user avatar
  • 6,256
4 votes
1 answer

Universe polymorphism and modules in Coq

The following code (without universe polymorphism) is accepted by Coq (8.16.0) : ...
Dave's user avatar
  • 175
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: ...
Matt Diamond's user avatar
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 ...
Trebor's user avatar
  • 4,015
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 ...
KANG Rongji's user avatar
8 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 ...
ice1000's user avatar
  • 6,256
15 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. ...
Sean O'Connor's user avatar
13 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 <...
ice1000's user avatar
  • 6,256
15 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 ...
ice1000's user avatar
  • 6,256