Zulip Chat Archive

Stream: general

Topic: Lean vs dependent type theory


view this post on Zulip Kenny Lau (Mar 17 2019 at 15:53):

Are there any difference between Lean's DTT and "regular" DTT?

view this post on Zulip Patrick Massot (Mar 17 2019 at 15:54):

There is no such thing as « regular DTT »

view this post on Zulip Kenny Lau (Mar 17 2019 at 15:57):

then what is "DTT"?

view this post on Zulip Patrick Massot (Mar 17 2019 at 16:00):

https://github.com/digama0/lean-type-theory

view this post on Zulip Patrick Massot (Mar 17 2019 at 16:02):

More seriously, I recommend watching at least the first three lectures in https://www.college-de-france.fr/site/xavier-leroy/course-2018-2019.htm

view this post on Zulip Wojciech Nawrocki (Mar 17 2019 at 16:03):

@Patrick Massot does a translation of those exist?

view this post on Zulip Patrick Massot (Mar 17 2019 at 16:26):

I don't think so

view this post on Zulip Patrick Massot (Mar 17 2019 at 16:28):

I posted this link because Kenny can understand any language

view this post on Zulip Mario Carneiro (Mar 17 2019 at 17:12):

"regular DTT" is probably Martin-Lof type theory

view this post on Zulip Mario Carneiro (Mar 17 2019 at 17:14):

that's lean without universes, inductives, the three axioms and proof irrelevance

view this post on Zulip Kevin Buzzard (Mar 17 2019 at 17:15):

So inductive types are not part of DTT?

view this post on Zulip Kevin Buzzard (Mar 17 2019 at 17:15):

that's lean without universes, inductives, the three axioms and proof irrelevance

Coq has all of those things, right?

view this post on Zulip Mario Carneiro (Mar 17 2019 at 17:18):

The Coq type system is called CIC (calculus of inductive constructions), and yes, inductives are the main addition

view this post on Zulip Mario Carneiro (Mar 17 2019 at 17:18):

coq doesn't have proof irrelevance


Last updated: May 14 2021 at 04:22 UTC