11
$\begingroup$

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.

$\endgroup$
3
  • 1
    $\begingroup$ 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). $\endgroup$
    – Jason Rute
    Mar 10, 2022 at 0:31
  • $\begingroup$ @JasonRute That's exactly what I meant, thanks! $\endgroup$
    – Trebor
    Mar 10, 2022 at 4:45
  • 1
    $\begingroup$ Is it meant to save time in the first place? Or is it just to ensure a broader generality/applicability of the results? $\endgroup$ Mar 11, 2022 at 8:21

1 Answer 1

3
$\begingroup$

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.

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.