Possible error in "Theorem proving in Lean"

Stream: general

[Roman Bars]

At the URL https://leanprover.github.io/theorem_proving_in_lean/inductive_types.html we find the sentence: "It is remarkable that it is possible to construct a substantial edifice of mathematics based on nothing more than the type universes, Pi types, and inductive types; everything else follows from those."

Is this correct? Specifically can we form the dependent pair types in terms of inductive types and Pi types?

[Eric Wieser]

src#sigma

[Eric Wieser]

Dependent pairs are just an inductive type with one constructor, whose second argument depends on its first

[Roman Bars]

Eric Wieser said:

Dependent pairs are just an inductive type with one constructor, whose second argument depends on its first

Can this be formulated in terms of W-types?

[Mario Carneiro]

If you formulate things in terms of W types, then you need a few other primitives to get all inductive types, and pairs are one of the primitives. The reduction to W-types is described in chapter 5 of my thesis https://github.com/digama0/lean-type-theory/releases/tag/v1.0

[Roman Bars]

Thank you Mario that's helpful.

[Mario Carneiro]

The eight primitive inductive types in that reduction are: false, Sigma, sum, ulift, nonempty, W, eq and acc

[Mario Carneiro]

Plus the primitives of DTT, i.e. pi types and universes