# Zulip Chat Archive

## 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?

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

#### 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):

Thank you Mario that's helpful.

#### Mario Carneiro (Mar 01 2021 at 14:35):

The eight primitive inductive types in that reduction are: `false`

, `Sigma`

, `sum`

, `ulift`

, `nonempty`

, `W`

, `eq`

and `acc`

#### Mario Carneiro (Mar 01 2021 at 14:36):

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

Last updated: Dec 20 2023 at 11:08 UTC