dependent type theory

Stream: new members

[Arthur Paulino]

Any recommendations on free material about dependent type theory? I'm looking for something that starts from the basics and is self-contained

[Mario Carneiro]

Have you looked at #tpil? The first few chapters are a gentle introduction to dependent type theory

[Johan Commelin]

The intro to the HoTT book is also appreciated by many.

[Arthur Paulino]

Mario Carneiro said:

Have you looked at #tpil? The first few chapters are a gentle introduction to dependent type theory

I was reading it but I was missing a bit of the "why"s

[Arthur Paulino]

Johan Commelin said:

The intro to the HoTT book is also appreciated by many.

Will check it out, thanks!

[Scott Morrison]

(More than the intro to the HoTT book: all of "Foundations" / "Type Theory". It's only at the "Homotopy type theory" that is diverges away from Lean's dependent type theory meaningfully.)

[Arthur Paulino]

@Scott Morrison what do you mean?

[Yaël Dillies]

You can read the HoTT book until the chapter "Homotopy type theory" because that's where the difference between homotopy type theory and dependent type theory starts.

[Scott Morrison]

Johan said "the intro to the HoTT book", and I was clarifying that you might want to read much more than the intro: rather all of section of 1 of part I.

[Arthur Paulino]

I see, thanks!

[Scott Morrison]

(And the next section on homotopy type theory is fascinating, if largely irrelevant to mathlib. It's good to think about how we might achieve the practical goodies of homotopy type theory without univalence, in any case: things like tactic#equiv_rw was the beginning of an attempt to provide tactics for "transport dependent types along a (some-structure-preserving) isomorphism".)

[Arthur Paulino]

Just to make sure, is this the book you are talking about?
https://hott.github.io/HoTT-2019/images/hott-intro-rijke.pdf

[Bryan Gin-ge Chen]

No, it's this one: https://homotopytypetheory.org/book/

[Lucas Teixeira]

I've found this book to be pretty good, although truthfully I'm still only a couple of chapters deep into it myself

https://www.amazon.com/Type-Theory-Formal-Proof-Introduction/dp/110703650X