Type Theory Beginner

Stream: new members

[Kevin Allen]

Hi, this is less of a Lean question and more of a 'general beginner' question.
Would it be recommended to study some Type Theory while learning Lean? I have no background in Type Theory and I am starting to study Category Theory (Steve Awodey's textbook). I noticed in 'Theorem Proving in Lean' there are chapters on Dependent Types and Inductive types so I will start making my way through that book, but are there any course notes or textbooks that someone can recommend?
Thanks. Much appreciated

[Johan Commelin]

What is your goal? And what is your background?

[Johan Commelin]

I never seriously studied any type theory. And I feel quite at home using lean.

[Bryan Gin-ge Chen]

I don't think anything outside of what's in TPiL is strictly necessary for just using Lean, but I found Nederpelt and Geuvers's "Type Theory and Formal Proof" fairly enlightening, even though it doesn't quite get to CIC (calculus of inductive constructions, which Lean's core type theory is based on).

[Kevin Allen]

Just trying to learn Lean in general but some of the discussions about type theory got me curious. My background is primarily in algebra and number theory so this is all new to me

[Kevin Allen]

and thanks! That's very helpful

[Johan Commelin]

If you are interested in the details: go for it.

But if your goal is to play around with algebra/number theory, then you can get very far by thinking Type = set.

[Kevin Buzzard]

If you're a mathematician then I would put off learning type theory. I taught a Lean course for mathematicians https://github.com/ImperialCollegeLondon/formalising-mathematics and I just told them "when Lean says G : Type just read it as "let $G$ be a set", and when it says g : G that means "let $g$ be an element of $G$".

[Kevin Buzzard]

Then we just got on with doing algebra/analysis/topology.

[Kevin Allen]

Thanks for the resource. This is all very reassuring :smile: