How much duplication does universe polymorphism actually save us?

Question

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.

Answer 1

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.