How to understand the sigma types example from "Theorem Proving in Lean 4"?

Question

In the Lean 4 book called "Theorem Proving in Lean 4" (https://lean-lang.org/theorem_proving_in_lean4/title_page.html), I don't understand a code example about cartesian product types in chapter 2 "Dependent Type Theory".

The example (which I have edited to keep only relevant information) is:

universe u v

def f (α : Type u) (β : α → Type v) (a : α) (b : β a) : (a : α) × β a :=
  ⟨a, b⟩

def h1 (x : Nat) : Nat :=
  (f Type (fun α => α) Nat x).2

#eval h1 5 -- 5

I would have written h1 as below:

def h1 (x : Nat) : Nat :=
  (f Nat (fun α => α) x x).2

I don't understand why the first argument of h1 has to be Type instead of the Nat concrete type since we told that the type of its first argument type is (α : Type u) i.e. α is a type like Nat. Don't we build pairs of naturals ?

After having read the comment of question Non-trivial examples of dependent sum ($\Sigma$-types) in Lean?, I understand that the first element of the pair has to be a type (and not a natural) which allows us to make the type of the second element depend on it. That brings two questions:

1. What is the role of universes u and v used in this example ? Is there an implicit hierarchy like u < v or u + 1 = v ? I think the concept of "universe" is not explained in the manual before meeting that example.
2. Could the type of the second element in the pair depend on a concrete value alone instead of a type ? Would it still be called a cartesian product dependent type ? See below.

def f' (_n : Nat) (β : Nat → Type v) (a : Nat) (b : β a) : (a : Nat) × β a := ⟨a, b⟩

def h1' (x : Nat) : Nat := (f Nat (fun _ => Nat) x x).2

#eval h1' 5 -- 5

Answer 1

1. Yes, there is a universe hierarchy. The role of universes is to let you manipulate types just like the elements of any other type, say Nat. So for instance, the list type family simply has type Type -> Type, without the need for a separate "type-level" quantification/function type like for polymorphic functions in OCaml for instance. The question then is "what is the type of Type?". If one goes the naïve way and asks that Type : Type, paradoxes ensue (an analog of Russel's paradox called Girard's paradox). The standard solution is to have a hierarchy of Type, Type 0 : Type 1 : …. But in practice, this is not very workable, as one wants to be more flexible. This is why most type-theoretic proof assistants implement a more relaxed approach, typically one where one uses variables for universe levels, together with a set of constraints, which ensures that there always exists an instantiation of the levels with integers in a sound way.

2. Yes, there is nothing forcing the first type to be Type. Your example is indeed still a cartesian product, albeit a slightly degenerate one (because the type of the second component does not depend on the first one). That way, you recover the usual non-dependent version of binary product. If you want a more interesting example, here is one

def g (b : Bool) : Type :=
  match b with
  | true => Nat
  | false => Bool

def h1'' (x : Nat) : Nat := (f Bool g true x).2

#eval h1'' 5

The function g really computes a type based on its argument.