type theory for mathematicians

Stream: maths

[Johan Commelin]

I'm looking for a short (e.g. 5 pages) introduction into type theory for professional mathematicians that have no familiarity with foundations/logic at all. So these people know what a vector bundle with connection is, or a quasi-coherent sheaf on a normal algebraic variety. But they don't know the turnstile symbol.
Any suggestions?

[Johan Commelin]

In particular it shouldn't focus on being constructive etc...

[Mario Carneiro]

Maybe something about HOL?

[Johan Commelin]

Maybe, I don't know HOL...

[Mario Carneiro]

those descriptions usually focus less on constructivity than systems derived from MLTT

[Mario Carneiro]

It's simple type theory

[Johan Commelin]

I just found http://www.nuprl.org/documents/Constable/naive.pdf but didn't read it yet

[Mario Carneiro]

computational type theory sounds like a red flag to me

[Johan Commelin]

but naive sounds good

[Mario Carneiro]

yeah that one is not what you want

[Mario Carneiro]

nuprl types are weird

[Johan Commelin]

I don't care if it is 5 pages of constructive stuff... as long as it isn't emphasised

[Johan Commelin]

I'm getting a bunch of questions about how type theory works and if it is similar to set theory or not. And I would like to point people to a gentle intro that contrasts the two

[Mario Carneiro]

https://golem.ph.utexas.edu/category/2013/01/from_set_theory_to_type_theory.html looks promising, although it will have a constructive bent

[Mario Carneiro]

What do you think about http://imps.mcmaster.ca/doc/seven-virtues.pdf

[Johan Commelin]

I've read the start of the Golem one, and it looks good. I'll now try the imps one

[Mario Carneiro]

the second one is about simple type theory but for someone who doesn't know what a type is it's best to start simple

[Johan Commelin]

I prefer the Golem one so far. The imps paper is still quite heavy on logical jargon. (If my eyes start to glaze over, then certainly this will happen to the people in my department who have never been exposed to formal logic or type theory before.)

[Mario Carneiro]

I think the golem one stays informal throughout, although it gets into univalence towards the end

[Johan Commelin]

Yeah, I don't care about univalence. But the informal part is really good I think.

[Mario Carneiro]

still it's good for conveying the "type theory" way of looking at things

[Johan Commelin]

Exactly

[Johan Commelin]

Apart from the final bit about univalence, this is exactly what I'm looking for! Thanks @Mario Carneiro

[Kenny Lau]

A type is just a set —Kevin Buzzard

[Reid Barton]

I was going to suggest "probably something written by Mike Shulman for the n-category cafe", but I see that's what Mario already found for you

[Kevin Buzzard]

Why not just tell them that type theory and set theory are equiconsistent?

[Kevin Buzzard]

And that a type is a set whose elements are terms, and a term is not a set

[Jeremy Avigad]

For what it's worth, here is something I wrote a while ago, after spending a year working on Feit-Thompson (and before the existence of Lean): https://arxiv.org/abs/1111.5885.