A collection of notes on various features commonly found in type theories whose definitions I always forget.
- Basic type theory (there are so many people who have already done this)
- First-order predicate logic in judgement form
- Types are propositions, terms are proofs, computation is proof simplification
- Syntax and judgement forms, positive vs. negative presentations
- The MLTT model (formation/introduction/elimination/computation/uniqueness rules)
- The PTS model (rules and axioms)
- Type universes (want!!)
- The universe hierarchy
- Russell vs. Tarski universes
- Cumulativity
- Impredicativity
- Girard's paradox
- Proof-irrelevant universes
- Limit universes
- Coinductive structures, M types, nu-types, corecursion
- Induction-recursion, induction-induction, higher inductive types (maybe not)
- Univalence, n-types (without going too much into HoTT)
- Add typing rules for dependent pairs and booleans in the appendix
- Remove introducing dependent eliminators from Notions of Equality
- "Judgemental equality" is not extensional equality, and no-one uses "computational equality"
- Fix DOT graph generation