• Type Theory and Formal Proofs

Type Theory and Formal Proofs

This is a partial formalization of the first few chapters of Type Theory and Formal Proof: An Introduction by Nederpelt and Geuvers in Coq. As it stands, the formalization covers up to approximately chapter 3.

I differ in a few places from their formalization. In particular, I use de Bruijn indices, simply because they are so much more convenient than worrying about α-conversion everywhere. I also include proofs of several exercises from the book.