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.
mathlib
you only need up toType 3
(or ZFC + 4 inaccessible cardinals) (which I understand is not exactly what you are asking for this question). $\endgroup$