Type-theoretic Foundations of Constructive Mathematics
From PBDN
Type-theoretic Foundations of Constructive Mathematics
Type-theoretic Foundations of Constructive Mathematics refers to a 49-page handout consisting of a 44-page extract from a draft of a book by Coquand, Dybjer, and Palmgren.
Two versions were handed out: one at the start of the year and a second on 24th September, 2007, which incorporates some corrections.
Since Prof. Palmgren has worked from this handout in about 3 lectures, the handout needs to be identified on some wiki pages. It is identified simply as "K" (for kompendium) by analogy with the compendia which exist for some other courses.