# Zulip Chat Archive

## Stream: general

### Topic: introductions to dependent type theory for mathematicians

#### Scott Morrison (Mar 15 2018 at 05:57):

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 (Mar 15 2018 at 05:59):

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

#### Simon Hudon (Mar 15 2018 at 06:00):

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 (Mar 15 2018 at 06:04):

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

#### Andrew Ashworth (Mar 15 2018 at 06:04):

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

#### Mario Carneiro (Mar 15 2018 at 06:05):

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

#### Mario Carneiro (Mar 15 2018 at 06:05):

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

#### Scott Morrison (Mar 15 2018 at 06:06):

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>.

Last updated: May 17 2021 at 21:12 UTC