Zulip Chat Archive

Stream: general

Topic: Possible error in "Theorem proving in Lean"


view this post on Zulip 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?

view this post on Zulip Eric Wieser (Mar 01 2021 at 14:03):

src#sigma

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Roman Bars (Mar 01 2021 at 14:34):

Thank you Mario that's helpful.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Mar 01 2021 at 14:36):

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


Last updated: May 15 2021 at 23:13 UTC