Section 1: Introductipn
A brief introduction to type theory in the context of the natural numbersSection 2: Propositions as Types
The Curry-Howard isomorphism and intuitionistic logic as formulated in type theory. Worked-out example of how to prove the associative law for the natural numbers using the Peano axioms. Discussion of dependent types and the predicate calculus, the Law of the Excluded Middle, higher order logics. Brief discussion of inference rules such as congruence.Section 3: Agda
The beginning of some notes on Agda. Rewrite.Section 4: Lambda Calculus
Bare-bones description of the syntax and semantics of the lambda calculus; normal forms and divergence ofSection 4: Type Inference
A sketch of the basic idea; unification.Section 4: Mathematical Notes
For now, just some remarks on the connection between the theory of groupoids and type theory.