See Notes on Constructive Type theory - for more details on most of lecture 7 and all of lecture 8.
See Lecture 9
Draft. Last Revised: 28th May, 1998.