Confusion from "Functional Programming in Lean" section 5.5

Stream: new members

[Garrison Venn]

In section 5.5 of "Functional Programming in Lean" the following is stated:

Function types occupy the smallest universe that can contain both the argument type and the return type. This means that Nat → Nat is a Type, Type → Type is a Type 1, and Type 3 is a Type 1 → Type 2.

Is the part: Type 3 is a Type 1 -> Type 2 incorrect? It seems it should be Type 2 (Sort 3), as the least upper bound of {1, 2} is 2?

I'm I missing something?

Thanks in advance

[Julian Berman]

(https://lean-lang.org/functional_programming_in_lean/Functors___-Applicative-Functors___-and-Monads/Universes/#universe-levels for reference)

Type 3 is a Type 4, as the paragraph just above says. What's happening on that line is that Type 3 and Type 1 \to Type 2 somehow got swapped -- the latter is a the-former.

I'm not sure how that happened, probably minor editing mistake, because it's correct in the old version of the book at https://leanprover.github.io/functional_programming_in_lean/functor-applicative-monad/universes.html

[Garrison Venn]

Thanks. Ok I think my confusion stems from using universe Type u for universe u. Using Sort instead I have: Type 1 -> Type 2 which translates to Type 1 is in Sort 3, Type 2 is in Sort 4, with the function type in Sort (max 3 4) = Sort 4. Therefore the function type lives in universe Type 3.

Is this correct? Sorry I'm being pedantic, but I've confused myself and AI to boot (which is always fun :-) ).

[Julian Berman]

Yes that looks right though I think personally I either convert everything to Sorts or everything to Types if I'm doing this in my head (which is rare) -- needless to say sitting in front of Lean and using #check or example to check what you say can be helpful to unconfuse yourself.

[Julian Berman]

But yeah if you want to use Sort, then Type 1 is Sort 2, Type 2 is Sort 3, so Type 1 \to Type 2 is Sort 2 \to Sort 3, Sort 3 lives in Sort 4, so that's the smallest universe that fits everything