Good introductory book to type theory?Formalization of mathematicsGood introductory text book on Matroid Theory?Motivating mathematics(particularly algebraic number theory) through historical problemsAlternative or reprint of Carter's “Finite Groups of Lie Type: Conjugacy Classes and Complex Characters”Does foundation/regularity have any categorical/structural consequences, in ZF?Consequences of foundation/regularity in ordinary mathematics (over ZF–AF)?What's the point of cubical type theory?Formal foundations done properlyHow can the simply typed lambda calculus be Turing-incomplete, yet stronger than second-order logic?Explaining the consistency of PRA and ZF from predicative foundationsFormalization of mathematics
Good introductory book to type theory?
Formalization of mathematicsGood introductory text book on Matroid Theory?Motivating mathematics(particularly algebraic number theory) through historical problemsAlternative or reprint of Carter's “Finite Groups of Lie Type: Conjugacy Classes and Complex Characters”Does foundation/regularity have any categorical/structural consequences, in ZF?Consequences of foundation/regularity in ordinary mathematics (over ZF–AF)?What's the point of cubical type theory?Formal foundations done properlyHow can the simply typed lambda calculus be Turing-incomplete, yet stronger than second-order logic?Explaining the consistency of PRA and ZF from predicative foundationsFormalization of mathematics
$begingroup$
I don't know anything about type theory but and I would like to learn it.
I'm interested to know how we can found mathematics on it.
So, I would be interested by any text about type theory whose angle is similar to the one of Russel and Whitehead in the Principia, or similar to the one of Bourbaki (for instance).
But, I am also interested by any nice presentation of type theory (without any special focus on foundation of mathematics) that would help me to get the best of it.
Books, texts, articles, links are welcomed.
I am interested by any type theory (Martin-Löf's, homotopic, etc.).
PS:
If it can help, in a way, by "foundation of mathematics", I mean "total formalization of mathematics", as in Bourbaki for instance.
PPS:
I have asked another related question there, a little bit more general.
reference-request lo.logic textbook-recommendation foundations type-theory
$endgroup$
|
show 2 more comments
$begingroup$
I don't know anything about type theory but and I would like to learn it.
I'm interested to know how we can found mathematics on it.
So, I would be interested by any text about type theory whose angle is similar to the one of Russel and Whitehead in the Principia, or similar to the one of Bourbaki (for instance).
But, I am also interested by any nice presentation of type theory (without any special focus on foundation of mathematics) that would help me to get the best of it.
Books, texts, articles, links are welcomed.
I am interested by any type theory (Martin-Löf's, homotopic, etc.).
PS:
If it can help, in a way, by "foundation of mathematics", I mean "total formalization of mathematics", as in Bourbaki for instance.
PPS:
I have asked another related question there, a little bit more general.
reference-request lo.logic textbook-recommendation foundations type-theory
$endgroup$
$begingroup$
Can you please explain a bit your mathematical and computer science background, so that we can suggest appropriate material. Have you studied logic, or topology, or have you encountered types (maybe in a programming language)?
$endgroup$
– Andrej Bauer
May 6 at 20:29
2
$begingroup$
Also, this should be a wiki question.
$endgroup$
– Andrej Bauer
May 6 at 20:29
$begingroup$
@AndrejBauer Since I'm looking for a text that would describe how to found mathematics, I'm sure my background is so relevant. When I quickly look at HoTT : Univalent foundations of mathematics, I don't see any explanation of "universes" or "types" or "function types" or what is the syntax of the language used, etc. I have a PhD in maths. I studied Algebraic Geometry, Topology, Algebra (commutative, differential), Categories (but not Toposes), etc.
$endgroup$
– Colas
May 6 at 21:17
2
$begingroup$
If you are looking for something more precise, perhaps Martin Escardo's lecture notes will help. They are very precise because they are written in Agda, and every detail is checked. But when you say that you want an "explanation", what is that supposed to be? It's a foundational theory, it introduces primitive notions. You can get used to these notions, and analogies with your pre-existing mathematical knowledge can be made, but there can be no precise explanation.
$endgroup$
– Andrej Bauer
May 6 at 22:08
$begingroup$
I am looking for a text where the « semantics » of types would be encoded in a formal syntax. If that makes sense to you.
$endgroup$
– Colas
May 6 at 22:14
|
show 2 more comments
$begingroup$
I don't know anything about type theory but and I would like to learn it.
I'm interested to know how we can found mathematics on it.
So, I would be interested by any text about type theory whose angle is similar to the one of Russel and Whitehead in the Principia, or similar to the one of Bourbaki (for instance).
But, I am also interested by any nice presentation of type theory (without any special focus on foundation of mathematics) that would help me to get the best of it.
Books, texts, articles, links are welcomed.
I am interested by any type theory (Martin-Löf's, homotopic, etc.).
PS:
If it can help, in a way, by "foundation of mathematics", I mean "total formalization of mathematics", as in Bourbaki for instance.
PPS:
I have asked another related question there, a little bit more general.
reference-request lo.logic textbook-recommendation foundations type-theory
$endgroup$
I don't know anything about type theory but and I would like to learn it.
I'm interested to know how we can found mathematics on it.
So, I would be interested by any text about type theory whose angle is similar to the one of Russel and Whitehead in the Principia, or similar to the one of Bourbaki (for instance).
But, I am also interested by any nice presentation of type theory (without any special focus on foundation of mathematics) that would help me to get the best of it.
Books, texts, articles, links are welcomed.
I am interested by any type theory (Martin-Löf's, homotopic, etc.).
PS:
If it can help, in a way, by "foundation of mathematics", I mean "total formalization of mathematics", as in Bourbaki for instance.
PPS:
I have asked another related question there, a little bit more general.
reference-request lo.logic textbook-recommendation foundations type-theory
reference-request lo.logic textbook-recommendation foundations type-theory
edited May 7 at 14:00
community wiki
6 revs, 3 users 100%
Colas
$begingroup$
Can you please explain a bit your mathematical and computer science background, so that we can suggest appropriate material. Have you studied logic, or topology, or have you encountered types (maybe in a programming language)?
$endgroup$
– Andrej Bauer
May 6 at 20:29
2
$begingroup$
Also, this should be a wiki question.
$endgroup$
– Andrej Bauer
May 6 at 20:29
$begingroup$
@AndrejBauer Since I'm looking for a text that would describe how to found mathematics, I'm sure my background is so relevant. When I quickly look at HoTT : Univalent foundations of mathematics, I don't see any explanation of "universes" or "types" or "function types" or what is the syntax of the language used, etc. I have a PhD in maths. I studied Algebraic Geometry, Topology, Algebra (commutative, differential), Categories (but not Toposes), etc.
$endgroup$
– Colas
May 6 at 21:17
2
$begingroup$
If you are looking for something more precise, perhaps Martin Escardo's lecture notes will help. They are very precise because they are written in Agda, and every detail is checked. But when you say that you want an "explanation", what is that supposed to be? It's a foundational theory, it introduces primitive notions. You can get used to these notions, and analogies with your pre-existing mathematical knowledge can be made, but there can be no precise explanation.
$endgroup$
– Andrej Bauer
May 6 at 22:08
$begingroup$
I am looking for a text where the « semantics » of types would be encoded in a formal syntax. If that makes sense to you.
$endgroup$
– Colas
May 6 at 22:14
|
show 2 more comments
$begingroup$
Can you please explain a bit your mathematical and computer science background, so that we can suggest appropriate material. Have you studied logic, or topology, or have you encountered types (maybe in a programming language)?
$endgroup$
– Andrej Bauer
May 6 at 20:29
2
$begingroup$
Also, this should be a wiki question.
$endgroup$
– Andrej Bauer
May 6 at 20:29
$begingroup$
@AndrejBauer Since I'm looking for a text that would describe how to found mathematics, I'm sure my background is so relevant. When I quickly look at HoTT : Univalent foundations of mathematics, I don't see any explanation of "universes" or "types" or "function types" or what is the syntax of the language used, etc. I have a PhD in maths. I studied Algebraic Geometry, Topology, Algebra (commutative, differential), Categories (but not Toposes), etc.
$endgroup$
– Colas
May 6 at 21:17
2
$begingroup$
If you are looking for something more precise, perhaps Martin Escardo's lecture notes will help. They are very precise because they are written in Agda, and every detail is checked. But when you say that you want an "explanation", what is that supposed to be? It's a foundational theory, it introduces primitive notions. You can get used to these notions, and analogies with your pre-existing mathematical knowledge can be made, but there can be no precise explanation.
$endgroup$
– Andrej Bauer
May 6 at 22:08
$begingroup$
I am looking for a text where the « semantics » of types would be encoded in a formal syntax. If that makes sense to you.
$endgroup$
– Colas
May 6 at 22:14
$begingroup$
Can you please explain a bit your mathematical and computer science background, so that we can suggest appropriate material. Have you studied logic, or topology, or have you encountered types (maybe in a programming language)?
$endgroup$
– Andrej Bauer
May 6 at 20:29
$begingroup$
Can you please explain a bit your mathematical and computer science background, so that we can suggest appropriate material. Have you studied logic, or topology, or have you encountered types (maybe in a programming language)?
$endgroup$
– Andrej Bauer
May 6 at 20:29
2
2
$begingroup$
Also, this should be a wiki question.
$endgroup$
– Andrej Bauer
May 6 at 20:29
$begingroup$
Also, this should be a wiki question.
$endgroup$
– Andrej Bauer
May 6 at 20:29
$begingroup$
@AndrejBauer Since I'm looking for a text that would describe how to found mathematics, I'm sure my background is so relevant. When I quickly look at HoTT : Univalent foundations of mathematics, I don't see any explanation of "universes" or "types" or "function types" or what is the syntax of the language used, etc. I have a PhD in maths. I studied Algebraic Geometry, Topology, Algebra (commutative, differential), Categories (but not Toposes), etc.
$endgroup$
– Colas
May 6 at 21:17
$begingroup$
@AndrejBauer Since I'm looking for a text that would describe how to found mathematics, I'm sure my background is so relevant. When I quickly look at HoTT : Univalent foundations of mathematics, I don't see any explanation of "universes" or "types" or "function types" or what is the syntax of the language used, etc. I have a PhD in maths. I studied Algebraic Geometry, Topology, Algebra (commutative, differential), Categories (but not Toposes), etc.
$endgroup$
– Colas
May 6 at 21:17
2
2
$begingroup$
If you are looking for something more precise, perhaps Martin Escardo's lecture notes will help. They are very precise because they are written in Agda, and every detail is checked. But when you say that you want an "explanation", what is that supposed to be? It's a foundational theory, it introduces primitive notions. You can get used to these notions, and analogies with your pre-existing mathematical knowledge can be made, but there can be no precise explanation.
$endgroup$
– Andrej Bauer
May 6 at 22:08
$begingroup$
If you are looking for something more precise, perhaps Martin Escardo's lecture notes will help. They are very precise because they are written in Agda, and every detail is checked. But when you say that you want an "explanation", what is that supposed to be? It's a foundational theory, it introduces primitive notions. You can get used to these notions, and analogies with your pre-existing mathematical knowledge can be made, but there can be no precise explanation.
$endgroup$
– Andrej Bauer
May 6 at 22:08
$begingroup$
I am looking for a text where the « semantics » of types would be encoded in a formal syntax. If that makes sense to you.
$endgroup$
– Colas
May 6 at 22:14
$begingroup$
I am looking for a text where the « semantics » of types would be encoded in a formal syntax. If that makes sense to you.
$endgroup$
– Colas
May 6 at 22:14
|
show 2 more comments
6 Answers
6
active
oldest
votes
$begingroup$
I am far from being an expert. I will make a few suggestions.
Per Martin-Löf. Intuitionistic type theory. (Notes by Giovanni Sambin of a series of lectures given in Padua, June 1980). Napoli, Bibliopolis, 1984
T. Streicher (1991), Semantics of Type Theory: Correctness, Completeness, and Independence Results, Birkhäuser Boston.
Andre Joyal. Notes on Clans and Tribes.
Michael Shulman. Homotopy type theory: the logic of space.
Thorsten Altenkirch. Naive Type Theory.
$endgroup$
8
$begingroup$
Streicher and Joyal are not introductory. Martin-Löf is a bit like trying to learn Christianity by reading the Bible.
$endgroup$
– Andrej Bauer
May 6 at 19:53
$begingroup$
Does one of these references emphasize on foundations of mathematics?
$endgroup$
– Colas
May 6 at 20:00
1
$begingroup$
@Colas: The only foundational narrative that I know about is in a beautiful paper by Shulman: sciencedirect.com/science/article/pii/…
$endgroup$
– Ivan Di Liberti
May 6 at 21:06
$begingroup$
@IvanDiLiberti Yes, that looks much more like what I'm looking for. Thanks
$endgroup$
– Colas
May 6 at 21:26
1
$begingroup$
@AndrejBauer For what it’s worth, I read that paper of Martin Lof and found it helped me understand type theory, but I already had a lot of experience programming Haskell and maybe a little Agda (i.e., direct knowledge of the divine). I think had also read “Proofs and Types” (which I would not recommend as an intro)
$endgroup$
– Izaak Meckler
May 7 at 1:16
|
show 2 more comments
$begingroup$
Here are some resources:
UniMath school teaching materials, and in particular:
Spartan type theory, an introduction to type theory (slides)
Introduction to Univalent Foundations of Mathematics with Agda by Martín Escardó.
Univalent Foundations programme: Homotopy Type Theory: Univalent Foundations of Mathematics
- Bengt Nordström, Kent Petersson, and Jan M. Smith: Programming in Martin-Löf's Type Theory
$endgroup$
2
$begingroup$
During my first experience with Type Theory, I had quite some troubles to understand your option 2, and in fact, I truly needed to get my hands on the option number 1 in my answer to understand something. I am not trying to defend my answer, the point I want to make is that different backgrounds and sensitivities might react very differently with our suggestions.
$endgroup$
– Ivan Di Liberti
May 6 at 20:09
2
$begingroup$
@IvanDiLiberti: I am well aware of the fact that type theory is difficult to learn and that not everyone likes the same approach. A lot depends on the background of the person who is learning. Actually, OP should explain their background a bit.
$endgroup$
– Andrej Bauer
May 6 at 20:28
add a comment |
$begingroup$
It seems that the HoTT book and Vladimir Voevodsky’s program for Univalent Foundations of Mathematics is made for you !
You will find everything from here:
https://homotopytypetheory.org/
$endgroup$
2
$begingroup$
Learning univalent foundations so you can understand Russell and Whitehead? Are you mad?
$endgroup$
– Nik Weaver
May 6 at 18:41
1
$begingroup$
@NikWeaver The original question is pretty vague - it's certainly not clear that the OP's intention is to understand Principia. Given that the OP seems to just want to learn something about any kind of type theoretic foundation for mathematics, steering them away from Russell and Whitehead toward something more modern seems wise!
$endgroup$
– Alex Kruckman
May 6 at 18:56
2
$begingroup$
@NikWeaver Although elementary type theory might be easy, "a la Russell and Whitehead" can be misleading. The type theory in Principia is a ramified type theory, which needs (or at least uses) a reducibility axiom to undo unwanted effects of the ramification.
$endgroup$
– Andreas Blass
May 6 at 20:15
2
$begingroup$
@NikWeaver I know you're well aware of anything related to predicativity. Nevertheless, I worried that your comment might send some readers to Principia with the intention of learning elementary type theory.
$endgroup$
– Andreas Blass
May 6 at 21:30
4
$begingroup$
When people mention type theory, what typically goes through my head is an extension of the simply typed lambda calculus. It is true that Russell stratified objects into types but this is a very different flavour to the utility of types in lambda calculus. For one, lambda calculus can be seen as a programming language, which leads to the whole subject of Curry-Howard correspondence about a duality between proofs and programs. This is the flavour of type theory I think Andrej is talking about. Other than the idea of typing, Russell's types have very little to do with this idea.
$endgroup$
– Ali Caglayan
May 6 at 22:27
|
show 10 more comments
$begingroup$
Dan Grayson's paper here is an exceptionally clear exposition. The first half or so is a useful introduction to type theory generally, even if you're not interested in univalence. The second half (on univalence) is even better.
$endgroup$
add a comment |
$begingroup$
This entry level overview of pure type systems might be helpful: http://www.rbjones.com/rbjpub/logic/cl/tlc004.htm
Roorda's masters' thesis http://www.staff.science.uu.nl/~jeuri101/MSc/jwroorda/thesis.ps goes into PTS further, though from a programming language theory perspective.
I've been wanting to read Barendregt's Lambda Calculus with Types: ftp://ftp.cs.ru.nl/pub/CompMath.Found/HBK.ps
This paper by Martin-Löf is pretty readable: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.131.926&rep=rep1&type=pdf
Also some lecture notes: http://intuitionistic.files.wordpress.com/2010/07/martin-lof-tt.pdf
There is a ton of stuff on ncatlab.org.
$endgroup$
add a comment |
$begingroup$
If your interest is type theoretic foundations, you might want to look into modern (type-theory based) theorem provers. This is how I learned both type theory and dependent type theory. This has the following advantages:
- Proof assistants let you "program in type theory". This ability to manipulate type theoretic objects (and have a compiler yell at you when you do something wrong) was really helpful for me.
- Like Principia Mathematica, modern theorem provers are designed to be foundations of mathematics that can be used to formally prove theorems in mathematics. And unlike ZFC (or even Principia), these systems are practically useable. (Now, "practical" is relative. They still are too cumbersome for a typical working mathematician, but they have nonetheless been used to formally prove a number of major theorems in mathematics.)
- The tutorials for these theorem provers are well-written, designed for a broad audience, and are not quite as intense as say the Homotopy Type Theory book.
There are some disadvantages to this approach.
- The tutorials I am about to list don't give much, if any, meta-theory on type theory. While they will teach you how to prove things in type theory, they don't give proofs about type theory.
- Another disadvantage is that they might be a bit more geared to those who are CS literate.
I am biased since one of the authors is my advisor, but Theorem proving in Lean is a great way to learn dependent type theory and the Lean proof assistant. It even has an online environment to try things out without having to install any software.
It is much older, but I also found the HOL-Light tutorial to be a good way to learn a weaker type-theoretic proof system.
$endgroup$
add a comment |
Your Answer
StackExchange.ready(function()
var channelOptions =
tags: "".split(" "),
id: "504"
;
initTagRenderer("".split(" "), "".split(" "), channelOptions);
StackExchange.using("externalEditor", function()
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled)
StackExchange.using("snippets", function()
createEditor();
);
else
createEditor();
);
function createEditor()
StackExchange.prepareEditor(
heartbeatType: 'answer',
autoActivateHeartbeat: false,
convertImagesToLinks: true,
noModals: true,
showLowRepImageUploadWarning: true,
reputationToPostImages: 10,
bindNavPrevention: true,
postfix: "",
imageUploader:
brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
allowUrls: true
,
noCode: true, onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
);
);
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function ()
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmathoverflow.net%2fquestions%2f330873%2fgood-introductory-book-to-type-theory%23new-answer', 'question_page');
);
Post as a guest
Required, but never shown
6 Answers
6
active
oldest
votes
6 Answers
6
active
oldest
votes
active
oldest
votes
active
oldest
votes
$begingroup$
I am far from being an expert. I will make a few suggestions.
Per Martin-Löf. Intuitionistic type theory. (Notes by Giovanni Sambin of a series of lectures given in Padua, June 1980). Napoli, Bibliopolis, 1984
T. Streicher (1991), Semantics of Type Theory: Correctness, Completeness, and Independence Results, Birkhäuser Boston.
Andre Joyal. Notes on Clans and Tribes.
Michael Shulman. Homotopy type theory: the logic of space.
Thorsten Altenkirch. Naive Type Theory.
$endgroup$
8
$begingroup$
Streicher and Joyal are not introductory. Martin-Löf is a bit like trying to learn Christianity by reading the Bible.
$endgroup$
– Andrej Bauer
May 6 at 19:53
$begingroup$
Does one of these references emphasize on foundations of mathematics?
$endgroup$
– Colas
May 6 at 20:00
1
$begingroup$
@Colas: The only foundational narrative that I know about is in a beautiful paper by Shulman: sciencedirect.com/science/article/pii/…
$endgroup$
– Ivan Di Liberti
May 6 at 21:06
$begingroup$
@IvanDiLiberti Yes, that looks much more like what I'm looking for. Thanks
$endgroup$
– Colas
May 6 at 21:26
1
$begingroup$
@AndrejBauer For what it’s worth, I read that paper of Martin Lof and found it helped me understand type theory, but I already had a lot of experience programming Haskell and maybe a little Agda (i.e., direct knowledge of the divine). I think had also read “Proofs and Types” (which I would not recommend as an intro)
$endgroup$
– Izaak Meckler
May 7 at 1:16
|
show 2 more comments
$begingroup$
I am far from being an expert. I will make a few suggestions.
Per Martin-Löf. Intuitionistic type theory. (Notes by Giovanni Sambin of a series of lectures given in Padua, June 1980). Napoli, Bibliopolis, 1984
T. Streicher (1991), Semantics of Type Theory: Correctness, Completeness, and Independence Results, Birkhäuser Boston.
Andre Joyal. Notes on Clans and Tribes.
Michael Shulman. Homotopy type theory: the logic of space.
Thorsten Altenkirch. Naive Type Theory.
$endgroup$
8
$begingroup$
Streicher and Joyal are not introductory. Martin-Löf is a bit like trying to learn Christianity by reading the Bible.
$endgroup$
– Andrej Bauer
May 6 at 19:53
$begingroup$
Does one of these references emphasize on foundations of mathematics?
$endgroup$
– Colas
May 6 at 20:00
1
$begingroup$
@Colas: The only foundational narrative that I know about is in a beautiful paper by Shulman: sciencedirect.com/science/article/pii/…
$endgroup$
– Ivan Di Liberti
May 6 at 21:06
$begingroup$
@IvanDiLiberti Yes, that looks much more like what I'm looking for. Thanks
$endgroup$
– Colas
May 6 at 21:26
1
$begingroup$
@AndrejBauer For what it’s worth, I read that paper of Martin Lof and found it helped me understand type theory, but I already had a lot of experience programming Haskell and maybe a little Agda (i.e., direct knowledge of the divine). I think had also read “Proofs and Types” (which I would not recommend as an intro)
$endgroup$
– Izaak Meckler
May 7 at 1:16
|
show 2 more comments
$begingroup$
I am far from being an expert. I will make a few suggestions.
Per Martin-Löf. Intuitionistic type theory. (Notes by Giovanni Sambin of a series of lectures given in Padua, June 1980). Napoli, Bibliopolis, 1984
T. Streicher (1991), Semantics of Type Theory: Correctness, Completeness, and Independence Results, Birkhäuser Boston.
Andre Joyal. Notes on Clans and Tribes.
Michael Shulman. Homotopy type theory: the logic of space.
Thorsten Altenkirch. Naive Type Theory.
$endgroup$
I am far from being an expert. I will make a few suggestions.
Per Martin-Löf. Intuitionistic type theory. (Notes by Giovanni Sambin of a series of lectures given in Padua, June 1980). Napoli, Bibliopolis, 1984
T. Streicher (1991), Semantics of Type Theory: Correctness, Completeness, and Independence Results, Birkhäuser Boston.
Andre Joyal. Notes on Clans and Tribes.
Michael Shulman. Homotopy type theory: the logic of space.
Thorsten Altenkirch. Naive Type Theory.
edited yesterday
community wiki
3 revs
Ivan Di Liberti
8
$begingroup$
Streicher and Joyal are not introductory. Martin-Löf is a bit like trying to learn Christianity by reading the Bible.
$endgroup$
– Andrej Bauer
May 6 at 19:53
$begingroup$
Does one of these references emphasize on foundations of mathematics?
$endgroup$
– Colas
May 6 at 20:00
1
$begingroup$
@Colas: The only foundational narrative that I know about is in a beautiful paper by Shulman: sciencedirect.com/science/article/pii/…
$endgroup$
– Ivan Di Liberti
May 6 at 21:06
$begingroup$
@IvanDiLiberti Yes, that looks much more like what I'm looking for. Thanks
$endgroup$
– Colas
May 6 at 21:26
1
$begingroup$
@AndrejBauer For what it’s worth, I read that paper of Martin Lof and found it helped me understand type theory, but I already had a lot of experience programming Haskell and maybe a little Agda (i.e., direct knowledge of the divine). I think had also read “Proofs and Types” (which I would not recommend as an intro)
$endgroup$
– Izaak Meckler
May 7 at 1:16
|
show 2 more comments
8
$begingroup$
Streicher and Joyal are not introductory. Martin-Löf is a bit like trying to learn Christianity by reading the Bible.
$endgroup$
– Andrej Bauer
May 6 at 19:53
$begingroup$
Does one of these references emphasize on foundations of mathematics?
$endgroup$
– Colas
May 6 at 20:00
1
$begingroup$
@Colas: The only foundational narrative that I know about is in a beautiful paper by Shulman: sciencedirect.com/science/article/pii/…
$endgroup$
– Ivan Di Liberti
May 6 at 21:06
$begingroup$
@IvanDiLiberti Yes, that looks much more like what I'm looking for. Thanks
$endgroup$
– Colas
May 6 at 21:26
1
$begingroup$
@AndrejBauer For what it’s worth, I read that paper of Martin Lof and found it helped me understand type theory, but I already had a lot of experience programming Haskell and maybe a little Agda (i.e., direct knowledge of the divine). I think had also read “Proofs and Types” (which I would not recommend as an intro)
$endgroup$
– Izaak Meckler
May 7 at 1:16
8
8
$begingroup$
Streicher and Joyal are not introductory. Martin-Löf is a bit like trying to learn Christianity by reading the Bible.
$endgroup$
– Andrej Bauer
May 6 at 19:53
$begingroup$
Streicher and Joyal are not introductory. Martin-Löf is a bit like trying to learn Christianity by reading the Bible.
$endgroup$
– Andrej Bauer
May 6 at 19:53
$begingroup$
Does one of these references emphasize on foundations of mathematics?
$endgroup$
– Colas
May 6 at 20:00
$begingroup$
Does one of these references emphasize on foundations of mathematics?
$endgroup$
– Colas
May 6 at 20:00
1
1
$begingroup$
@Colas: The only foundational narrative that I know about is in a beautiful paper by Shulman: sciencedirect.com/science/article/pii/…
$endgroup$
– Ivan Di Liberti
May 6 at 21:06
$begingroup$
@Colas: The only foundational narrative that I know about is in a beautiful paper by Shulman: sciencedirect.com/science/article/pii/…
$endgroup$
– Ivan Di Liberti
May 6 at 21:06
$begingroup$
@IvanDiLiberti Yes, that looks much more like what I'm looking for. Thanks
$endgroup$
– Colas
May 6 at 21:26
$begingroup$
@IvanDiLiberti Yes, that looks much more like what I'm looking for. Thanks
$endgroup$
– Colas
May 6 at 21:26
1
1
$begingroup$
@AndrejBauer For what it’s worth, I read that paper of Martin Lof and found it helped me understand type theory, but I already had a lot of experience programming Haskell and maybe a little Agda (i.e., direct knowledge of the divine). I think had also read “Proofs and Types” (which I would not recommend as an intro)
$endgroup$
– Izaak Meckler
May 7 at 1:16
$begingroup$
@AndrejBauer For what it’s worth, I read that paper of Martin Lof and found it helped me understand type theory, but I already had a lot of experience programming Haskell and maybe a little Agda (i.e., direct knowledge of the divine). I think had also read “Proofs and Types” (which I would not recommend as an intro)
$endgroup$
– Izaak Meckler
May 7 at 1:16
|
show 2 more comments
$begingroup$
Here are some resources:
UniMath school teaching materials, and in particular:
Spartan type theory, an introduction to type theory (slides)
Introduction to Univalent Foundations of Mathematics with Agda by Martín Escardó.
Univalent Foundations programme: Homotopy Type Theory: Univalent Foundations of Mathematics
- Bengt Nordström, Kent Petersson, and Jan M. Smith: Programming in Martin-Löf's Type Theory
$endgroup$
2
$begingroup$
During my first experience with Type Theory, I had quite some troubles to understand your option 2, and in fact, I truly needed to get my hands on the option number 1 in my answer to understand something. I am not trying to defend my answer, the point I want to make is that different backgrounds and sensitivities might react very differently with our suggestions.
$endgroup$
– Ivan Di Liberti
May 6 at 20:09
2
$begingroup$
@IvanDiLiberti: I am well aware of the fact that type theory is difficult to learn and that not everyone likes the same approach. A lot depends on the background of the person who is learning. Actually, OP should explain their background a bit.
$endgroup$
– Andrej Bauer
May 6 at 20:28
add a comment |
$begingroup$
Here are some resources:
UniMath school teaching materials, and in particular:
Spartan type theory, an introduction to type theory (slides)
Introduction to Univalent Foundations of Mathematics with Agda by Martín Escardó.
Univalent Foundations programme: Homotopy Type Theory: Univalent Foundations of Mathematics
- Bengt Nordström, Kent Petersson, and Jan M. Smith: Programming in Martin-Löf's Type Theory
$endgroup$
2
$begingroup$
During my first experience with Type Theory, I had quite some troubles to understand your option 2, and in fact, I truly needed to get my hands on the option number 1 in my answer to understand something. I am not trying to defend my answer, the point I want to make is that different backgrounds and sensitivities might react very differently with our suggestions.
$endgroup$
– Ivan Di Liberti
May 6 at 20:09
2
$begingroup$
@IvanDiLiberti: I am well aware of the fact that type theory is difficult to learn and that not everyone likes the same approach. A lot depends on the background of the person who is learning. Actually, OP should explain their background a bit.
$endgroup$
– Andrej Bauer
May 6 at 20:28
add a comment |
$begingroup$
Here are some resources:
UniMath school teaching materials, and in particular:
Spartan type theory, an introduction to type theory (slides)
Introduction to Univalent Foundations of Mathematics with Agda by Martín Escardó.
Univalent Foundations programme: Homotopy Type Theory: Univalent Foundations of Mathematics
- Bengt Nordström, Kent Petersson, and Jan M. Smith: Programming in Martin-Löf's Type Theory
$endgroup$
Here are some resources:
UniMath school teaching materials, and in particular:
Spartan type theory, an introduction to type theory (slides)
Introduction to Univalent Foundations of Mathematics with Agda by Martín Escardó.
Univalent Foundations programme: Homotopy Type Theory: Univalent Foundations of Mathematics
- Bengt Nordström, Kent Petersson, and Jan M. Smith: Programming in Martin-Löf's Type Theory
edited May 7 at 14:00
community wiki
2 revs, 2 users 95%
Andrej Bauer
2
$begingroup$
During my first experience with Type Theory, I had quite some troubles to understand your option 2, and in fact, I truly needed to get my hands on the option number 1 in my answer to understand something. I am not trying to defend my answer, the point I want to make is that different backgrounds and sensitivities might react very differently with our suggestions.
$endgroup$
– Ivan Di Liberti
May 6 at 20:09
2
$begingroup$
@IvanDiLiberti: I am well aware of the fact that type theory is difficult to learn and that not everyone likes the same approach. A lot depends on the background of the person who is learning. Actually, OP should explain their background a bit.
$endgroup$
– Andrej Bauer
May 6 at 20:28
add a comment |
2
$begingroup$
During my first experience with Type Theory, I had quite some troubles to understand your option 2, and in fact, I truly needed to get my hands on the option number 1 in my answer to understand something. I am not trying to defend my answer, the point I want to make is that different backgrounds and sensitivities might react very differently with our suggestions.
$endgroup$
– Ivan Di Liberti
May 6 at 20:09
2
$begingroup$
@IvanDiLiberti: I am well aware of the fact that type theory is difficult to learn and that not everyone likes the same approach. A lot depends on the background of the person who is learning. Actually, OP should explain their background a bit.
$endgroup$
– Andrej Bauer
May 6 at 20:28
2
2
$begingroup$
During my first experience with Type Theory, I had quite some troubles to understand your option 2, and in fact, I truly needed to get my hands on the option number 1 in my answer to understand something. I am not trying to defend my answer, the point I want to make is that different backgrounds and sensitivities might react very differently with our suggestions.
$endgroup$
– Ivan Di Liberti
May 6 at 20:09
$begingroup$
During my first experience with Type Theory, I had quite some troubles to understand your option 2, and in fact, I truly needed to get my hands on the option number 1 in my answer to understand something. I am not trying to defend my answer, the point I want to make is that different backgrounds and sensitivities might react very differently with our suggestions.
$endgroup$
– Ivan Di Liberti
May 6 at 20:09
2
2
$begingroup$
@IvanDiLiberti: I am well aware of the fact that type theory is difficult to learn and that not everyone likes the same approach. A lot depends on the background of the person who is learning. Actually, OP should explain their background a bit.
$endgroup$
– Andrej Bauer
May 6 at 20:28
$begingroup$
@IvanDiLiberti: I am well aware of the fact that type theory is difficult to learn and that not everyone likes the same approach. A lot depends on the background of the person who is learning. Actually, OP should explain their background a bit.
$endgroup$
– Andrej Bauer
May 6 at 20:28
add a comment |
$begingroup$
It seems that the HoTT book and Vladimir Voevodsky’s program for Univalent Foundations of Mathematics is made for you !
You will find everything from here:
https://homotopytypetheory.org/
$endgroup$
2
$begingroup$
Learning univalent foundations so you can understand Russell and Whitehead? Are you mad?
$endgroup$
– Nik Weaver
May 6 at 18:41
1
$begingroup$
@NikWeaver The original question is pretty vague - it's certainly not clear that the OP's intention is to understand Principia. Given that the OP seems to just want to learn something about any kind of type theoretic foundation for mathematics, steering them away from Russell and Whitehead toward something more modern seems wise!
$endgroup$
– Alex Kruckman
May 6 at 18:56
2
$begingroup$
@NikWeaver Although elementary type theory might be easy, "a la Russell and Whitehead" can be misleading. The type theory in Principia is a ramified type theory, which needs (or at least uses) a reducibility axiom to undo unwanted effects of the ramification.
$endgroup$
– Andreas Blass
May 6 at 20:15
2
$begingroup$
@NikWeaver I know you're well aware of anything related to predicativity. Nevertheless, I worried that your comment might send some readers to Principia with the intention of learning elementary type theory.
$endgroup$
– Andreas Blass
May 6 at 21:30
4
$begingroup$
When people mention type theory, what typically goes through my head is an extension of the simply typed lambda calculus. It is true that Russell stratified objects into types but this is a very different flavour to the utility of types in lambda calculus. For one, lambda calculus can be seen as a programming language, which leads to the whole subject of Curry-Howard correspondence about a duality between proofs and programs. This is the flavour of type theory I think Andrej is talking about. Other than the idea of typing, Russell's types have very little to do with this idea.
$endgroup$
– Ali Caglayan
May 6 at 22:27
|
show 10 more comments
$begingroup$
It seems that the HoTT book and Vladimir Voevodsky’s program for Univalent Foundations of Mathematics is made for you !
You will find everything from here:
https://homotopytypetheory.org/
$endgroup$
2
$begingroup$
Learning univalent foundations so you can understand Russell and Whitehead? Are you mad?
$endgroup$
– Nik Weaver
May 6 at 18:41
1
$begingroup$
@NikWeaver The original question is pretty vague - it's certainly not clear that the OP's intention is to understand Principia. Given that the OP seems to just want to learn something about any kind of type theoretic foundation for mathematics, steering them away from Russell and Whitehead toward something more modern seems wise!
$endgroup$
– Alex Kruckman
May 6 at 18:56
2
$begingroup$
@NikWeaver Although elementary type theory might be easy, "a la Russell and Whitehead" can be misleading. The type theory in Principia is a ramified type theory, which needs (or at least uses) a reducibility axiom to undo unwanted effects of the ramification.
$endgroup$
– Andreas Blass
May 6 at 20:15
2
$begingroup$
@NikWeaver I know you're well aware of anything related to predicativity. Nevertheless, I worried that your comment might send some readers to Principia with the intention of learning elementary type theory.
$endgroup$
– Andreas Blass
May 6 at 21:30
4
$begingroup$
When people mention type theory, what typically goes through my head is an extension of the simply typed lambda calculus. It is true that Russell stratified objects into types but this is a very different flavour to the utility of types in lambda calculus. For one, lambda calculus can be seen as a programming language, which leads to the whole subject of Curry-Howard correspondence about a duality between proofs and programs. This is the flavour of type theory I think Andrej is talking about. Other than the idea of typing, Russell's types have very little to do with this idea.
$endgroup$
– Ali Caglayan
May 6 at 22:27
|
show 10 more comments
$begingroup$
It seems that the HoTT book and Vladimir Voevodsky’s program for Univalent Foundations of Mathematics is made for you !
You will find everything from here:
https://homotopytypetheory.org/
$endgroup$
It seems that the HoTT book and Vladimir Voevodsky’s program for Univalent Foundations of Mathematics is made for you !
You will find everything from here:
https://homotopytypetheory.org/
answered May 6 at 18:30
community wiki
L. Garde
2
$begingroup$
Learning univalent foundations so you can understand Russell and Whitehead? Are you mad?
$endgroup$
– Nik Weaver
May 6 at 18:41
1
$begingroup$
@NikWeaver The original question is pretty vague - it's certainly not clear that the OP's intention is to understand Principia. Given that the OP seems to just want to learn something about any kind of type theoretic foundation for mathematics, steering them away from Russell and Whitehead toward something more modern seems wise!
$endgroup$
– Alex Kruckman
May 6 at 18:56
2
$begingroup$
@NikWeaver Although elementary type theory might be easy, "a la Russell and Whitehead" can be misleading. The type theory in Principia is a ramified type theory, which needs (or at least uses) a reducibility axiom to undo unwanted effects of the ramification.
$endgroup$
– Andreas Blass
May 6 at 20:15
2
$begingroup$
@NikWeaver I know you're well aware of anything related to predicativity. Nevertheless, I worried that your comment might send some readers to Principia with the intention of learning elementary type theory.
$endgroup$
– Andreas Blass
May 6 at 21:30
4
$begingroup$
When people mention type theory, what typically goes through my head is an extension of the simply typed lambda calculus. It is true that Russell stratified objects into types but this is a very different flavour to the utility of types in lambda calculus. For one, lambda calculus can be seen as a programming language, which leads to the whole subject of Curry-Howard correspondence about a duality between proofs and programs. This is the flavour of type theory I think Andrej is talking about. Other than the idea of typing, Russell's types have very little to do with this idea.
$endgroup$
– Ali Caglayan
May 6 at 22:27
|
show 10 more comments
2
$begingroup$
Learning univalent foundations so you can understand Russell and Whitehead? Are you mad?
$endgroup$
– Nik Weaver
May 6 at 18:41
1
$begingroup$
@NikWeaver The original question is pretty vague - it's certainly not clear that the OP's intention is to understand Principia. Given that the OP seems to just want to learn something about any kind of type theoretic foundation for mathematics, steering them away from Russell and Whitehead toward something more modern seems wise!
$endgroup$
– Alex Kruckman
May 6 at 18:56
2
$begingroup$
@NikWeaver Although elementary type theory might be easy, "a la Russell and Whitehead" can be misleading. The type theory in Principia is a ramified type theory, which needs (or at least uses) a reducibility axiom to undo unwanted effects of the ramification.
$endgroup$
– Andreas Blass
May 6 at 20:15
2
$begingroup$
@NikWeaver I know you're well aware of anything related to predicativity. Nevertheless, I worried that your comment might send some readers to Principia with the intention of learning elementary type theory.
$endgroup$
– Andreas Blass
May 6 at 21:30
4
$begingroup$
When people mention type theory, what typically goes through my head is an extension of the simply typed lambda calculus. It is true that Russell stratified objects into types but this is a very different flavour to the utility of types in lambda calculus. For one, lambda calculus can be seen as a programming language, which leads to the whole subject of Curry-Howard correspondence about a duality between proofs and programs. This is the flavour of type theory I think Andrej is talking about. Other than the idea of typing, Russell's types have very little to do with this idea.
$endgroup$
– Ali Caglayan
May 6 at 22:27
2
2
$begingroup$
Learning univalent foundations so you can understand Russell and Whitehead? Are you mad?
$endgroup$
– Nik Weaver
May 6 at 18:41
$begingroup$
Learning univalent foundations so you can understand Russell and Whitehead? Are you mad?
$endgroup$
– Nik Weaver
May 6 at 18:41
1
1
$begingroup$
@NikWeaver The original question is pretty vague - it's certainly not clear that the OP's intention is to understand Principia. Given that the OP seems to just want to learn something about any kind of type theoretic foundation for mathematics, steering them away from Russell and Whitehead toward something more modern seems wise!
$endgroup$
– Alex Kruckman
May 6 at 18:56
$begingroup$
@NikWeaver The original question is pretty vague - it's certainly not clear that the OP's intention is to understand Principia. Given that the OP seems to just want to learn something about any kind of type theoretic foundation for mathematics, steering them away from Russell and Whitehead toward something more modern seems wise!
$endgroup$
– Alex Kruckman
May 6 at 18:56
2
2
$begingroup$
@NikWeaver Although elementary type theory might be easy, "a la Russell and Whitehead" can be misleading. The type theory in Principia is a ramified type theory, which needs (or at least uses) a reducibility axiom to undo unwanted effects of the ramification.
$endgroup$
– Andreas Blass
May 6 at 20:15
$begingroup$
@NikWeaver Although elementary type theory might be easy, "a la Russell and Whitehead" can be misleading. The type theory in Principia is a ramified type theory, which needs (or at least uses) a reducibility axiom to undo unwanted effects of the ramification.
$endgroup$
– Andreas Blass
May 6 at 20:15
2
2
$begingroup$
@NikWeaver I know you're well aware of anything related to predicativity. Nevertheless, I worried that your comment might send some readers to Principia with the intention of learning elementary type theory.
$endgroup$
– Andreas Blass
May 6 at 21:30
$begingroup$
@NikWeaver I know you're well aware of anything related to predicativity. Nevertheless, I worried that your comment might send some readers to Principia with the intention of learning elementary type theory.
$endgroup$
– Andreas Blass
May 6 at 21:30
4
4
$begingroup$
When people mention type theory, what typically goes through my head is an extension of the simply typed lambda calculus. It is true that Russell stratified objects into types but this is a very different flavour to the utility of types in lambda calculus. For one, lambda calculus can be seen as a programming language, which leads to the whole subject of Curry-Howard correspondence about a duality between proofs and programs. This is the flavour of type theory I think Andrej is talking about. Other than the idea of typing, Russell's types have very little to do with this idea.
$endgroup$
– Ali Caglayan
May 6 at 22:27
$begingroup$
When people mention type theory, what typically goes through my head is an extension of the simply typed lambda calculus. It is true that Russell stratified objects into types but this is a very different flavour to the utility of types in lambda calculus. For one, lambda calculus can be seen as a programming language, which leads to the whole subject of Curry-Howard correspondence about a duality between proofs and programs. This is the flavour of type theory I think Andrej is talking about. Other than the idea of typing, Russell's types have very little to do with this idea.
$endgroup$
– Ali Caglayan
May 6 at 22:27
|
show 10 more comments
$begingroup$
Dan Grayson's paper here is an exceptionally clear exposition. The first half or so is a useful introduction to type theory generally, even if you're not interested in univalence. The second half (on univalence) is even better.
$endgroup$
add a comment |
$begingroup$
Dan Grayson's paper here is an exceptionally clear exposition. The first half or so is a useful introduction to type theory generally, even if you're not interested in univalence. The second half (on univalence) is even better.
$endgroup$
add a comment |
$begingroup$
Dan Grayson's paper here is an exceptionally clear exposition. The first half or so is a useful introduction to type theory generally, even if you're not interested in univalence. The second half (on univalence) is even better.
$endgroup$
Dan Grayson's paper here is an exceptionally clear exposition. The first half or so is a useful introduction to type theory generally, even if you're not interested in univalence. The second half (on univalence) is even better.
answered May 8 at 15:09
community wiki
Steven Landsburg
add a comment |
add a comment |
$begingroup$
This entry level overview of pure type systems might be helpful: http://www.rbjones.com/rbjpub/logic/cl/tlc004.htm
Roorda's masters' thesis http://www.staff.science.uu.nl/~jeuri101/MSc/jwroorda/thesis.ps goes into PTS further, though from a programming language theory perspective.
I've been wanting to read Barendregt's Lambda Calculus with Types: ftp://ftp.cs.ru.nl/pub/CompMath.Found/HBK.ps
This paper by Martin-Löf is pretty readable: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.131.926&rep=rep1&type=pdf
Also some lecture notes: http://intuitionistic.files.wordpress.com/2010/07/martin-lof-tt.pdf
There is a ton of stuff on ncatlab.org.
$endgroup$
add a comment |
$begingroup$
This entry level overview of pure type systems might be helpful: http://www.rbjones.com/rbjpub/logic/cl/tlc004.htm
Roorda's masters' thesis http://www.staff.science.uu.nl/~jeuri101/MSc/jwroorda/thesis.ps goes into PTS further, though from a programming language theory perspective.
I've been wanting to read Barendregt's Lambda Calculus with Types: ftp://ftp.cs.ru.nl/pub/CompMath.Found/HBK.ps
This paper by Martin-Löf is pretty readable: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.131.926&rep=rep1&type=pdf
Also some lecture notes: http://intuitionistic.files.wordpress.com/2010/07/martin-lof-tt.pdf
There is a ton of stuff on ncatlab.org.
$endgroup$
add a comment |
$begingroup$
This entry level overview of pure type systems might be helpful: http://www.rbjones.com/rbjpub/logic/cl/tlc004.htm
Roorda's masters' thesis http://www.staff.science.uu.nl/~jeuri101/MSc/jwroorda/thesis.ps goes into PTS further, though from a programming language theory perspective.
I've been wanting to read Barendregt's Lambda Calculus with Types: ftp://ftp.cs.ru.nl/pub/CompMath.Found/HBK.ps
This paper by Martin-Löf is pretty readable: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.131.926&rep=rep1&type=pdf
Also some lecture notes: http://intuitionistic.files.wordpress.com/2010/07/martin-lof-tt.pdf
There is a ton of stuff on ncatlab.org.
$endgroup$
This entry level overview of pure type systems might be helpful: http://www.rbjones.com/rbjpub/logic/cl/tlc004.htm
Roorda's masters' thesis http://www.staff.science.uu.nl/~jeuri101/MSc/jwroorda/thesis.ps goes into PTS further, though from a programming language theory perspective.
I've been wanting to read Barendregt's Lambda Calculus with Types: ftp://ftp.cs.ru.nl/pub/CompMath.Found/HBK.ps
This paper by Martin-Löf is pretty readable: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.131.926&rep=rep1&type=pdf
Also some lecture notes: http://intuitionistic.files.wordpress.com/2010/07/martin-lof-tt.pdf
There is a ton of stuff on ncatlab.org.
answered May 7 at 23:11
community wiki
none
add a comment |
add a comment |
$begingroup$
If your interest is type theoretic foundations, you might want to look into modern (type-theory based) theorem provers. This is how I learned both type theory and dependent type theory. This has the following advantages:
- Proof assistants let you "program in type theory". This ability to manipulate type theoretic objects (and have a compiler yell at you when you do something wrong) was really helpful for me.
- Like Principia Mathematica, modern theorem provers are designed to be foundations of mathematics that can be used to formally prove theorems in mathematics. And unlike ZFC (or even Principia), these systems are practically useable. (Now, "practical" is relative. They still are too cumbersome for a typical working mathematician, but they have nonetheless been used to formally prove a number of major theorems in mathematics.)
- The tutorials for these theorem provers are well-written, designed for a broad audience, and are not quite as intense as say the Homotopy Type Theory book.
There are some disadvantages to this approach.
- The tutorials I am about to list don't give much, if any, meta-theory on type theory. While they will teach you how to prove things in type theory, they don't give proofs about type theory.
- Another disadvantage is that they might be a bit more geared to those who are CS literate.
I am biased since one of the authors is my advisor, but Theorem proving in Lean is a great way to learn dependent type theory and the Lean proof assistant. It even has an online environment to try things out without having to install any software.
It is much older, but I also found the HOL-Light tutorial to be a good way to learn a weaker type-theoretic proof system.
$endgroup$
add a comment |
$begingroup$
If your interest is type theoretic foundations, you might want to look into modern (type-theory based) theorem provers. This is how I learned both type theory and dependent type theory. This has the following advantages:
- Proof assistants let you "program in type theory". This ability to manipulate type theoretic objects (and have a compiler yell at you when you do something wrong) was really helpful for me.
- Like Principia Mathematica, modern theorem provers are designed to be foundations of mathematics that can be used to formally prove theorems in mathematics. And unlike ZFC (or even Principia), these systems are practically useable. (Now, "practical" is relative. They still are too cumbersome for a typical working mathematician, but they have nonetheless been used to formally prove a number of major theorems in mathematics.)
- The tutorials for these theorem provers are well-written, designed for a broad audience, and are not quite as intense as say the Homotopy Type Theory book.
There are some disadvantages to this approach.
- The tutorials I am about to list don't give much, if any, meta-theory on type theory. While they will teach you how to prove things in type theory, they don't give proofs about type theory.
- Another disadvantage is that they might be a bit more geared to those who are CS literate.
I am biased since one of the authors is my advisor, but Theorem proving in Lean is a great way to learn dependent type theory and the Lean proof assistant. It even has an online environment to try things out without having to install any software.
It is much older, but I also found the HOL-Light tutorial to be a good way to learn a weaker type-theoretic proof system.
$endgroup$
add a comment |
$begingroup$
If your interest is type theoretic foundations, you might want to look into modern (type-theory based) theorem provers. This is how I learned both type theory and dependent type theory. This has the following advantages:
- Proof assistants let you "program in type theory". This ability to manipulate type theoretic objects (and have a compiler yell at you when you do something wrong) was really helpful for me.
- Like Principia Mathematica, modern theorem provers are designed to be foundations of mathematics that can be used to formally prove theorems in mathematics. And unlike ZFC (or even Principia), these systems are practically useable. (Now, "practical" is relative. They still are too cumbersome for a typical working mathematician, but they have nonetheless been used to formally prove a number of major theorems in mathematics.)
- The tutorials for these theorem provers are well-written, designed for a broad audience, and are not quite as intense as say the Homotopy Type Theory book.
There are some disadvantages to this approach.
- The tutorials I am about to list don't give much, if any, meta-theory on type theory. While they will teach you how to prove things in type theory, they don't give proofs about type theory.
- Another disadvantage is that they might be a bit more geared to those who are CS literate.
I am biased since one of the authors is my advisor, but Theorem proving in Lean is a great way to learn dependent type theory and the Lean proof assistant. It even has an online environment to try things out without having to install any software.
It is much older, but I also found the HOL-Light tutorial to be a good way to learn a weaker type-theoretic proof system.
$endgroup$
If your interest is type theoretic foundations, you might want to look into modern (type-theory based) theorem provers. This is how I learned both type theory and dependent type theory. This has the following advantages:
- Proof assistants let you "program in type theory". This ability to manipulate type theoretic objects (and have a compiler yell at you when you do something wrong) was really helpful for me.
- Like Principia Mathematica, modern theorem provers are designed to be foundations of mathematics that can be used to formally prove theorems in mathematics. And unlike ZFC (or even Principia), these systems are practically useable. (Now, "practical" is relative. They still are too cumbersome for a typical working mathematician, but they have nonetheless been used to formally prove a number of major theorems in mathematics.)
- The tutorials for these theorem provers are well-written, designed for a broad audience, and are not quite as intense as say the Homotopy Type Theory book.
There are some disadvantages to this approach.
- The tutorials I am about to list don't give much, if any, meta-theory on type theory. While they will teach you how to prove things in type theory, they don't give proofs about type theory.
- Another disadvantage is that they might be a bit more geared to those who are CS literate.
I am biased since one of the authors is my advisor, but Theorem proving in Lean is a great way to learn dependent type theory and the Lean proof assistant. It even has an online environment to try things out without having to install any software.
It is much older, but I also found the HOL-Light tutorial to be a good way to learn a weaker type-theoretic proof system.
answered May 8 at 0:23
community wiki
Jason Rute
add a comment |
add a comment |
Thanks for contributing an answer to MathOverflow!
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
Use MathJax to format equations. MathJax reference.
To learn more, see our tips on writing great answers.
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function ()
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmathoverflow.net%2fquestions%2f330873%2fgood-introductory-book-to-type-theory%23new-answer', 'question_page');
);
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
$begingroup$
Can you please explain a bit your mathematical and computer science background, so that we can suggest appropriate material. Have you studied logic, or topology, or have you encountered types (maybe in a programming language)?
$endgroup$
– Andrej Bauer
May 6 at 20:29
2
$begingroup$
Also, this should be a wiki question.
$endgroup$
– Andrej Bauer
May 6 at 20:29
$begingroup$
@AndrejBauer Since I'm looking for a text that would describe how to found mathematics, I'm sure my background is so relevant. When I quickly look at HoTT : Univalent foundations of mathematics, I don't see any explanation of "universes" or "types" or "function types" or what is the syntax of the language used, etc. I have a PhD in maths. I studied Algebraic Geometry, Topology, Algebra (commutative, differential), Categories (but not Toposes), etc.
$endgroup$
– Colas
May 6 at 21:17
2
$begingroup$
If you are looking for something more precise, perhaps Martin Escardo's lecture notes will help. They are very precise because they are written in Agda, and every detail is checked. But when you say that you want an "explanation", what is that supposed to be? It's a foundational theory, it introduces primitive notions. You can get used to these notions, and analogies with your pre-existing mathematical knowledge can be made, but there can be no precise explanation.
$endgroup$
– Andrej Bauer
May 6 at 22:08
$begingroup$
I am looking for a text where the « semantics » of types would be encoded in a formal syntax. If that makes sense to you.
$endgroup$
– Colas
May 6 at 22:14