How to write a definition of the non-dependent product using Pi types in Lean?

Question

I'm working through chapter 7 – Inductive Types of "Theorem Proving in Lean".

I'd like to know how to write the definition of dependent non-dependent product in a more expanded or "primitive" form.

1. It looks like the definition given in the tutorial automatically infers some detail: inductive prod1 (α : Type u) (β : Type v) | mk : α → β → prod1

2. Some experimentation allows to fill in the detail inductive prod2 (α : Type u) (β : Type v) : Type (max u v) | mk : α → β → prod2

3. However giving the definition in a fully expand form, using Pi types fails to typecheck: inductive prod3 : Π (α : Type u) (β : Type v), Type (max u v) | mk : α → β → prod3

What is the correct way to write prod3?

Finally, is the following definition equivalent to prod1 and prod2, i.e. can the type checker always infer the correct type universe for α and β?

4. inductive prod4 (α : Type) (β : Type) | mk : α → β → prod4

Answer 1

First off, note that there is nothing dependent about your types. Dependent product is just another name for the Pi type itself (the Pi deriving from the usual mathematical notation for indexed products).

Your prod2 type is the correct maximally explicit version of prod1. In prod3, you changed α and β from inductive parameters to indices, which as you noticed doesn't work out for universe-related reasons. In general, indices are used to define inductive type families as in section 7.7.

Finally, the atomic Type you used in prod4 is an abbreviation of Type 1. You can use Type* to have universe parameters inferred automatically.