Zulip Chat Archive

Stream: maths

Topic: type theory for mathematicians


view this post on Zulip Johan Commelin (Feb 21 2019 at 10:38):

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?

view this post on Zulip Johan Commelin (Feb 21 2019 at 10:39):

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

view this post on Zulip Mario Carneiro (Feb 21 2019 at 10:40):

Maybe something about HOL?

view this post on Zulip Johan Commelin (Feb 21 2019 at 10:41):

Maybe, I don't know HOL...

view this post on Zulip Mario Carneiro (Feb 21 2019 at 10:41):

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

view this post on Zulip Mario Carneiro (Feb 21 2019 at 10:41):

It's simple type theory

view this post on Zulip Johan Commelin (Feb 21 2019 at 10:41):

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

view this post on Zulip Mario Carneiro (Feb 21 2019 at 10:41):

computational type theory sounds like a red flag to me

view this post on Zulip Johan Commelin (Feb 21 2019 at 10:42):

but naive sounds good

view this post on Zulip Mario Carneiro (Feb 21 2019 at 10:42):

yeah that one is not what you want

view this post on Zulip Mario Carneiro (Feb 21 2019 at 10:42):

nuprl types are weird

view this post on Zulip Johan Commelin (Feb 21 2019 at 10:42):

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

view this post on Zulip Johan Commelin (Feb 21 2019 at 10:43):

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

view this post on Zulip Mario Carneiro (Feb 21 2019 at 10:44):

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

view this post on Zulip Mario Carneiro (Feb 21 2019 at 10:48):

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

view this post on Zulip Johan Commelin (Feb 21 2019 at 10:48):

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

view this post on Zulip Mario Carneiro (Feb 21 2019 at 10:49):

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

view this post on Zulip Johan Commelin (Feb 21 2019 at 10:56):

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

view this post on Zulip Mario Carneiro (Feb 21 2019 at 10:57):

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

view this post on Zulip Johan Commelin (Feb 21 2019 at 10:57):

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

view this post on Zulip Mario Carneiro (Feb 21 2019 at 10:58):

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

view this post on Zulip Johan Commelin (Feb 21 2019 at 11:01):

Exactly

view this post on Zulip Johan Commelin (Feb 21 2019 at 11:19):

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

view this post on Zulip Kenny Lau (Feb 21 2019 at 12:12):

A type is just a set —Kevin Buzzard

view this post on Zulip Reid Barton (Feb 21 2019 at 13:41):

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

view this post on Zulip Kevin Buzzard (Feb 21 2019 at 15:10):

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

view this post on Zulip Kevin Buzzard (Feb 21 2019 at 15:10):

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

view this post on Zulip Jeremy Avigad (Feb 22 2019 at 01:16):

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.


Last updated: May 10 2021 at 07:15 UTC