I have been reading Martin Löf notes on type theory to get a historical feel for the subject and I find some of the terminology confusing (e.g. distinction judgements and propositions, between proofs and derivations in a formal system, and between sets/types and categories, etc.) It seems modern treatments of type theory (HoTT, etc.) do not require these discussions and such fine distinctions and opt to jump right into the rules of type theory. Is there a reason for this, beyond pedagogy?

My ultimate goal is to get up to speed with HoTT, but many experts mention that reading the HoTT book with out a strong background is not helpful. What supplementary sources would you suggest?

Martin Löf notes: https://archive-pml.github.io/martin-lof/pdfs/Bibliopolis-Book-retypeset-1984.pdf



You must log in to answer this question.

Browse other questions tagged .