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 to read.
• Clear up some important misunderstandings.

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

• (Ongoing) Models for dependent types
• Explanation of coherence problem
• Rewritten introduction for locally cartesian closed categories

• STLC
  • Rewrite combinator canonicity
  • Normalization for STLC
• Category theory
  • Rewrite LCCC part
  • Write about comprehension categories
  • Higher models
    • Groupoid model (elaborate)
    • Groupoid model as model category
    • Model category as type theoretic models (Types as fibrations!!)
    • Infinity category
• Misc
  • Typesetting, clean up bibliography
  • [\![]\!] is too annoying, maybe macro
  • Use separate font for metavariables?
  • Cite Tom de Jong's stuff?
  • Mention forcing & realizability?
  • Cite 1lab properly
  • Use fancyvrb to improve code display?

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.

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