Why to use a new type for every variable in definitions?

Stream: mathlib4

[Esteban Martínez Vañó]

Hi everyone.

While learning I've always stated my structures, theorems and definitions in such a way that I assign to every "free" variable the type ´´Type´, but when looking at the documentation in Mathlib I see that the usual way to do it is to assign to every new variable a type Type u_i.

What is the reason for doing that?

[Daniel Weber]

It's simply more general (it lets you treat the surreals as a field, for instance), and there's not much reason not to do that

[Daniel Weber]

In Mathlib there's Type* which means "a type in an arbitrary universe", you can usually just write it in place of Type

[Kevin Buzzard]

If you're interested in "big" objects such as the class of ordinals or the category of sets then you need to use higher universes to express these, so mathlib tries to make everything universe-polymorphic as you've spotted. In my undergraduate lean course, which gives examples of how to use lean to do basic stuff in ring theory, analysis, calculus etc I just use Type, I don't even introduce universes in the course, and it works fine, but I don't do any category theory or set theory in that course. As Daniel says, the reason they're there is that there's no reason not for them to be there.

Yesterday I noticed a higher universe in some pretty basic code I was writing when I was using Type not Type* (I often develop using Type and then just add the *s at the end when PRing, because occasionally being maximally polymorphic can cause confusing errors). Even though I was using Type := Type 0, I saw some intermediate universe u=1. I chased it down to a use of Finite G. In set theory Finite would be defined as a first order predicate on all sets and thus it's expressible without universes. In Mathlib it's defined as a function from Type to Prop and as such it lives in a higher universe because it's a function but (using set-theoretic language) its domain is not a set, it's a class.

[Esteban Martínez Vañó]

I see. I think I get it. But then, in practice, you don't write ´Type u_i´ for all the varaibles, just ´Type*´ and that makes them belong to the universe they need to be in?

[Kevin Buzzard]

Yes, (X : Type*) just means "create a new universe variable u_37 and make X live in that universe".

[Esteban Martínez Vañó]

I see.

But then, what is the problem in this code that works perfectly fine when I substitute every Type* by Type?

[Edward van de Meent]

the issue is that s is in the wrong universe. you can fix this by either adapting the construction you're using, or make Net have only one universe parameter (i.e. saying that X lives in the same universe as Net.D)

[Edward van de Meent]

as a third alternative, you can restrict your statement to ∀ (s : Net.{u_1,u_1} X)

[Kevin Buzzard]

/- Definition of net -/
structure Net (X: Type*) where
  D: Type*
  [directedSet: DirectedSet D]
  net : D → X

This is probably a bad definition in the sense that there are universes mentioned in the data of the definition which aren't mentioned in the statement. In situations like this I would do universe u and (X : Type u) and then D : Type u as well. For example the truth of some statements about nets might depend on the universe type chosen for D, and you don't really want that (you won't see the universe in the statement of the theorem, in fact you'll probably get an error that Lean can't figure out which universe you're talking about).

[Esteban Martínez Vañó]

Understood. Thanks!

So, for example, when stating that a sequence is a net, which I've done like this:

-- Every linear order is a directed set

instance LinearOrder.instDirectedSet {X : Type*} [LinearOrder X] [Inhabited X] : DirectedSet X where
  directed := by
    intro d e
    use max d e
    exact And.intro (le_max_left d e) (le_max_right d e)

-- ℕ (with its usual order relation) is a directed set and so every sequence is a net

@[simps]
instance Net.instSequences {X: Type} (s: ℕ → X) : Net X := Net.mk' (inferInstance) s

I must state that X has type Type, and not use Type*, because ℕ has type Type, isn't it?

[Edward van de Meent]

no. the issue is that Net depends on two universe parameters, while only one gets mentioned when you use it as a type.

[Esteban Martínez Vañó]

Sorry, I mean after changing the definition of Net as you and Kevin mentioned by making it depending on only one universe

[Edward van de Meent]

after that, you likely shouldn't need to change X to be Type.
indeed.

[Kyle Miller]

You can be explicit with universes too. I'm not necessarily recommending this here, but just so you know, this is possible:

structure Net.{v, u} (X : Type u) where
  D : Type v
  [directedSet : DirectedSet D]
  net : D → X

#check Net.{0, 0} Nat
-- The second `0` is inferred from `Nat`, so you can do this for short:
#check Net.{0} Nat

Notice I put v first in Net's universe level list to make the second #check possible to write.