introductions to dependent type theory for mathematicians

Stream: general

[Scott Morrison]

At tea today some colleagues expressed interest in learning about dependent type theory (interactive theorem proving may still be a bridge too far... :-). Does anyone have favourite recommendations for introductions, especially written for a "working mathematician" audience?

[Simon Hudon]

I'd be curious to see how far you can go using type theory as a tool without type checker

[Simon Hudon]

My angle on the subject has of course only been from the user's perspective so I'll admit that there's probably a whole world I know nothing about

[Andrew Ashworth]

hmm, i would recommend ncatlab to a mathematician... the references section seems through

[Andrew Ashworth]

https://ncatlab.org/nlab/show/dependent+type+theory

[Mario Carneiro]

I think the HoTT book is the best introduction to dependent type theory from a mathematician perspective

[Mario Carneiro]

just remember to get off the bus when they start talking about iterated identity types :)

[Scott Morrison]

Great! I'm very happy that my first two suggestions have been echoed here. :-) I also like Mike Schulman's post at <https://golem.ph.utexas.edu/category/2010/03/in_praise_of_dependent_types.html>.