Skip to main content
15 votes
Accepted

In Agda, why is universe polymorphism explicit?

First of all, you may simplify your code with the keyword: ...
ice1000's user avatar
  • 6,176
14 votes
Accepted

Why did Agda give up cumulative universes?

One reason (not particularly specific to Agda) might be that eta reduction is not compatible with cumulativity. With cumulativity (that is $Set_0 \leq Set_1$), and given \begin{align*} f &:= \...
Couchy's user avatar
  • 2,221
10 votes

What's the difference between a universe level and a natural number?

Modularity. Clearly, universe levels must form a semi-lattice with a successor. But there is no need to force it to be the set of natural numbers. Doing so would actually result in spurious ...
Pierre-Marie Pédrot's user avatar
9 votes
Accepted

What happened to Conor McBride's universe polymorphism proposal?

I don’t know for sure, but I don’t think this has been explored, no. At least I can say for sure it’s not around in Coq’s world (yes, time has passed and Coq now has universe polymorphism), although I ...
Meven Lennon-Bertrand's user avatar
8 votes
Accepted

What's the difference between a universe level and a natural number?

One of the things that make universe levels “just work”, to some extent, is that they satisfy the idempotent commutative monoid laws judgementally. This means that any elimination form of a universe ...
James Wood's user avatar
  • 1,053
7 votes

In Agda, why is universe polymorphism explicit?

In Agda, universe levels are not only explicit but they are also first class. This means that you can store them in data structures and compute with them. This allows you to write generic programs in ...
gallais's user avatar
  • 1,126
6 votes

Universe inconsistency errors when using ZF model in Coq

Here is how I would go about formalizing first-order logic and models, with a small fragment of ZF as an example. Note that we can still carry out Gödel coding by natural numbers, so long as the types ...
Andrej Bauer's user avatar
  • 9,104
5 votes
Accepted

Cardinality of Type in a given universe

Equality is not provable. Indeed, it is consistent that univ.{u u+1} < #(Type u) at every level u. Recall that the universe ...
François G. Dorais's user avatar
5 votes

What's the difference between a universe level and a natural number?

The biggest syntactic difference in the given two languages is that universe levels do not have an eliminator as natural numbers do. For instance, you can pattern match over a natural number, and you ...
ice1000's user avatar
  • 6,176
4 votes
Accepted

Is there any universe polymorphic version of univalence?

At least in papers on cubical type theory, 'respecting equivalence' is somewhat independent of universes. There is a judgmental notion of paths: $$Γ,i ⊢ T\ \mathsf{type} \\ Γ,i ⊢ t : T$$ The top being ...
Dan Doel's user avatar
  • 982
4 votes
Accepted

Universe polymorphism and modules in Coq

If you go polymorphic, you should probably go all the way, and also use a polymorphic product type, like so: ...
Meven Lennon-Bertrand's user avatar
3 votes
Accepted

Universe polymorphism and Coq standard library

Sadly, at the moment, there are no standard-ish libraries using universe polymorphism. A similar question arose some time ago and the Coq Zulip, and it seems multiple people from multiple projects ...
Meven Lennon-Bertrand's user avatar
3 votes
Accepted

How much duplication does universe polymorphism actually save us?

I don't have a statistical conclusion (I wish this question is still answerable without statistical analysis :D), but my impression on universe levels is that we usually use up to 2 different levels ...
ice1000's user avatar
  • 6,176
2 votes

What's the difference between a universe level and a natural number?

At some point in history, Agda's universe levels were just an inductive type like the naturals, but with different accompanying BUILTIN declarations so that they ...
Dan Doel's user avatar
  • 982
2 votes
Accepted

Lean 4: How can I specify that out of two universe variables, one is larger than the other?

I found the versions already in Mathlib. (I used moogle.ai to find it.) The one universe variable version: ...
Jason Rute's user avatar
  • 8,655
1 vote
Accepted

Universe inconsistency errors when using ZF model in Coq

Not sure exactly how your problem appears since you do not give the code up to the point where you get your failures so I cannot reproduce. But here is a self-contained example that should do the ...
Meven Lennon-Bertrand's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible