History of type theory 类型论简史

You can download the artifacts at the releases page.

你可以在此下载编译好的文件.

An overview of the history of type theory, mainly for mathematically oriented people. I seek to achive these goals:

• Provide a coherent and up-to-date source of information in Chinese.
• Link to important books and papers I recommend reading.
• Clear up some important misunderstandings.

This is my coursework. I have already finished the submitted version d0aaf51, but this is still being actively expanded (mostly during winter/summer holidays though). Suggestions and PR's are welcome!

Recent updates

• Switched to natural models
• Normalization fo STLC

TODO

• STLC
  • Rewrite combinator canonicity
  • Normalization for STLC
• Category theory
  • Natural models
  • Higher models
    • Groupoid model (elaborate)
    • Infinity categories and model categories
• Misc
  • Typesetting, clean up bibliography
  • Hyphen or en-dash between math and Chinese?
    • $\lambda$-演算, $p$-进数, etc.
  • [\![]\!] is too annoying, maybe macro
  • Use separate font for metavariables?
  • Cite Tom de Jong's stuff?
  • Mention forcing & realizability?
  • Cite 1lab properly

Conventions

As a self-note here are some conventions:

• ASCII punctuation, except for quotes, colons and anything ASCII doesn't have.
• Keep category magic to minimum, so there is a gradient of prerequisites. I can't make this completely self-contained, so there will be stuff that goes unexplained.
• Never ever use English jargon, unless discussing the matter of translation. However, use latin names faithfully. On the other hand, it would be asking too much to use Cyrillic or the Arabic script. So I will just note the spelling in the original language, and proceed to use latin transliterations.

License

This work is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International License.