The Type Theory Zoo

A collection of notes on various features commonly found in type theories whose definitions I always forget.

Planned Topics (a wishful list)

• 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)

TODOs

• 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