# 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 question is, how much duplication does that really save? In more precise words, if we are to write a major math library without universe polymorphism, how many copies of theorems and definitions would we have to add?

I assume that this can be easily calculated on existing libraries like mathlib. If I remember correctly, there was some discussion on universe levels in the Lean Zulip chat with the conclusion that we needed at most 5 or 6 different universe levels. But here I'm interested in how many different levels do we require a single definition to be on.

• Is this the Zulip conversation you had in mind (I'm using the public link)? leanprover-community.github.io/archive/stream/113488-general/… Mario's calculation at the time says in Lean's mathlib you only need up to Type 3 (or ZFC + 4 inaccessible cardinals) (which I understand is not exactly what you are asking for this question). Mar 10, 2022 at 0:31
• @JasonRute That's exactly what I meant, thanks!
– Trebor
Mar 10, 2022 at 4:45
• Is it meant to save time in the first place? Or is it just to ensure a broader generality/applicability of the results? Mar 11, 2022 at 8:21

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 in a bunch (like a file or several files on one topic) of code, and in rare cases we use slightly more (no more than 5 in my impression). Well, simply think about mathematics: when we talk about small sets or small cats, we are like assuming a polymorphic level and we're referring to things on that level, and we use "larger sets/cats" to refer to the next level. In a lot of cases, we just need these two levels.

So, it may seem that universe polymorphism just allows us to avoid the two (or maybe a little more) extra copies, right? You asked precisely this in the question, and now I want to make a claim against this point. It can actually save more copies. Here's why.

Let's look at a part of the definition of category in Arend's library:

\class Precat \plevels obj >= hom (Ob : \hType obj)
| Hom : Ob -> Ob -> \Set hom


It has two polymorphic levels, so if we have the potential of using 3 levels for each level parameter, there will be 6 copies (because you assumed obj level is greater than or equal to hom). Then, all category-related theorems will be copied along with the definition of category. Now, let's look at the agda-categories library's version of category:

record Category (o ℓ e : Level) : Set (suc (o ⊔ ℓ ⊔ e)) where
eta-equality
infix  4 _≈_ _⇒_
infixr 9 _∘_

field
Obj : Set o
_⇒_ : Rel Obj ℓ
_≈_ : ∀ {A B} → Rel (A ⇒ B) e


Agda does not support constraining level parameters, so all of these can be arbitrary, and there might be $$3^3=27$$ copies, if all parameters are likely to be specified to 3 different levels. Enriched category is worse:

    record Category (v : Level) : Set (o ⊔ ℓ ⊔ e ⊔ suc v) where
field
Obj : Set v


I think all of the above arguments are overgeneralizing on numbers, but the point is that working universe-polymorphically is still highly nontrivial (especially when everybody does it differently -- Arend supports level assumptions, Lean does not, Agda doesn't even have cumulativity by default, and I don't really know how Coq does it) due to the ability of working with multiple levels in one definition.

• If you want sheer number of independent levels, Functor has 6, PseudoFunctor has 8 and Bifunctor has 9 (in agda-categories). Mar 16, 2022 at 13:17