Type Theory topics

Date: 13 December 2018

This is a list of the main topics, sometimes with corresponding examples, for the type theory we study.

• Recursive definitions: e.g. summing a list.
• First-class functions: e.g. $\sum_{k=1}^{n} f(k)$.
• Fibonacci numbers: indirect recursion
• Currying: Ackermann function (illustrates not only primitve recursize)
  • A(0, n) = n + 1
  • A(m, 0) = A(m -1, 1)
  • A(m, n) = A(m - 1, A(m, n -1))
• Type Families:
  • e.g. tuples
  • e.g. reversing tuples, including searching by type
• Propositions as types:
  • e.g. subtraction
  • propositional combinations
  • quantification
  • basic examples as inductive types
  • Decidable type; Collatz function
• Inductive types
  • e.g. trees, dependent pairs
  • rec and induc terms
• Indexed Inductive types
  • e.g. Fin type family
  • induc in the indexed case
• Equality type
  • path induction principle
  • groupoid operations and their logical counterparts.

All notes