## Stream: general

### Topic: Possible error in "Theorem proving in Lean"

#### Roman Bars (Mar 01 2021 at 14:03):

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?

src#sigma

#### Eric Wieser (Mar 01 2021 at 14:04):

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

#### Roman Bars (Mar 01 2021 at 14:10):

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 (Mar 01 2021 at 14:32):

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 (Mar 01 2021 at 14:34):

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