[Intro to HoTT - OLD] Martin-Löf Type Theory: Judgments, Contexts, and Types 

Video 1 of the Martin-Löf Type Theory lecture, part of the Introduction to Homotopy Type Theory video lecture series. Covers the key mechanisms of formal MLTT: judgments, contexts, inference rules, and how to introduce new types.
This lecture series roughly follows Egbert Rijke's forthcoming textbook, Introduction to Homotopy Type Theory, which is expected to be released in 2021 by Cambridge University Press. More information can be found here: ncatlab.org/nlab/show/Introdu....
Some relevant resources:
- Paragraph about judgments in the nLab: ncatlab.org/nlab/show/judgmen...
- Article I wrote (which others have improved/maintained) describing the bool type in Standard ML: smlhelp.github.io/book/types/...
- SEP article on Theophrastus, the inventor(?) of modus ponens: plato.stanford.edu/entries/th...
- Wikipedia article on product spaces in classical topology: en.wikipedia.org/wiki/Product...
- Some lecture slides I made about the simply-typed lambda calculus and cartesian closed categories (compare the definition of the STLC in Section 1 with how we're defining MLTT here): jacobneu.github.io/teaching/C...