README

This development formalises the notions from the first few lectures on
Type Theory Foundations at OPLSS 2011.

* Overview of the development:
** Syntax
   Defines the syntax of the language and some notations. Nothing fancy.
** Substitution
   Defines substitutions for de Bruijn indices. Pretty much the most boring
   thing possible.
** Semantics
   Defines static and dynamic semantics of the language, proves the standard
   properties: weakening, progress, preservation, etc. and lemmas needed by
   termination proof that are not related to logical relations.
** Termination
   Defines the reducibility relation and proceeds to prove head expansion
   and termination.
** Equivalence
   Defines contexts and context typings, observable equivalence and logical equivalence,
   and proves soundness of logical equivalence wrt observable equivalence. Provdies one
   example of a logical equivalence (x : ω ⊢ x ∼ x + 0 : ω).