Typing out the lambda-pi tutorial. I didn't do the bits about adding data types, just the core calculus.