Zulip Chat Archive
Stream: general
Topic: Lean vs dependent type theory
Kenny Lau (Mar 17 2019 at 15:53):
Are there any difference between Lean's DTT and "regular" DTT?
Patrick Massot (Mar 17 2019 at 15:54):
There is no such thing as « regular DTT »
Kenny Lau (Mar 17 2019 at 15:57):
then what is "DTT"?
Patrick Massot (Mar 17 2019 at 16:00):
https://github.com/digama0/lean-type-theory
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
Wojciech Nawrocki (Mar 17 2019 at 16:03):
@Patrick Massot does a translation of those exist?
Patrick Massot (Mar 17 2019 at 16:26):
I don't think so
Patrick Massot (Mar 17 2019 at 16:28):
I posted this link because Kenny can understand any language
Mario Carneiro (Mar 17 2019 at 17:12):
"regular DTT" is probably Martin-Lof type theory
Mario Carneiro (Mar 17 2019 at 17:14):
that's lean without universes, inductives, the three axioms and proof irrelevance
Kevin Buzzard (Mar 17 2019 at 17:15):
So inductive types are not part of DTT?
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?
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
Mario Carneiro (Mar 17 2019 at 17:18):
coq doesn't have proof irrelevance
Last updated: Dec 20 2023 at 11:08 UTC