This introduction is fantastic. I don’t think I’ve seen something as comprehensive, clear and short as this before.
Edit: That said, I would have loved it if you introduced a few exercises throughout, or perhaps spoilered the types of some objects so people who are new to the area could guess things in advance. I remember a lot of things clicked for me when I set about trying to “discover” the type theory formalism myself.
I am also very happy about this; I learned something new, and the explanations felt perfectly clear.
Especially I liked the explanations “from outside perspective”, like lambda notation vs arrow notation, or why the product symbol is used. These things are typically not mentioned in textbooks, because they teach the official notation, but this is exactly what you need as a beginner, to connect what you already know with the new things.
This introduction is fantastic. I don’t think I’ve seen something as comprehensive, clear and short as this before.
Edit:
That said, I would have loved it if you introduced a few exercises throughout, or perhaps spoilered the types of some objects so people who are new to the area could guess things in advance. I remember a lot of things clicked for me when I set about trying to “discover” the type theory formalism myself.
I am also very happy about this; I learned something new, and the explanations felt perfectly clear.
Especially I liked the explanations “from outside perspective”, like lambda notation vs arrow notation, or why the product symbol is used. These things are typically not mentioned in textbooks, because they teach the official notation, but this is exactly what you need as a beginner, to connect what you already know with the new things.